[examples/lambda] fix duplicate theorem error in previous commit

HOL-Theorem-Prover · Nov 5, 2023 · 79234d8 · 79234d8
1 parent 34b7ae8
commit 79234d8
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/examples/lambda/other-models/pdbTransferScript.sml b/examples/lambda/other-models/pdbTransferScript.sml
@@ -152,7 +152,7 @@ val xfer = transfer_thm 10 [] true (global_ruledb()) o GEN_ALL
 
 Theorem dhreduce1_APP = xfer hreduce1_APP
 Theorem dhreduce1_BETA = xfer $ cj 1 hreduce1_rules
-Theorem dhreduce1_APP = xfer hreduce1_APP
+Theorem dhreduce1_LAM = xfer hreduce1_LAM
 Theorem dhreduce1_substitutive = xfer hreduce1_substitutive
 Theorem dhreduce1_rwts = xfer hreduce1_rwts
 Theorem dhreduce_substitutive = xfer hreduce_substitutive