[examples/lambda] fix proof broken by making fromTerm_11 automatic

HOL-Theorem-Prover · Nov 5, 2023 · f62315a · f62315a
1 parent 79234d8
commit f62315a
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/examples/lambda/completeness/boehm_treeScript.sml b/examples/lambda/completeness/boehm_treeScript.sml
@@ -110,7 +110,7 @@ Proof
  >> Know ‘fromTerm (toTerm M) = fromTerm (LAMl vs (VAR y @* args))’
  >- (art [fromTerm_11])
  >> Q.PAT_X_ASSUM ‘toTerm M = LAMl vs (VAR y @* args)’ K_TAC
- >> rw [fromTerm_LAMl, fromTerm_appstar]
+ >> rw [fromTerm_LAMl, fromTerm_appstar, Excl "fromTerm_11"]
  >> qabbrev_tac ‘vs' = MAP s2n vs’
  >> qabbrev_tac ‘Ms = MAP fromTerm args’
  >> qabbrev_tac ‘y' = s2n y’