From f62315a1fd068fc6bb1d4e27507f61097efd09a3 Mon Sep 17 00:00:00 2001
From: Michael Norrish <michael.norrish@anu.edu.au>
Date: Mon, 6 Nov 2023 10:42:59 +1100
Subject: [PATCH] [examples/lambda] fix proof broken by making fromTerm_11
 automatic

---
 examples/lambda/completeness/boehm_treeScript.sml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/examples/lambda/completeness/boehm_treeScript.sml b/examples/lambda/completeness/boehm_treeScript.sml
index 60fc697118..345268fa53 100644
--- 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’