From cbf165f01258b1e3d4f325d1e849520e87d4ee71 Mon Sep 17 00:00:00 2001
From: Michael Norrish <michael.norrish@anu.edu.au>
Date: Tue, 5 Jul 2022 09:32:46 +1000
Subject: [PATCH] Fix a couple of proofs broken by recent HOL changes

---
 compiler/parsing/fromSexpScript.sml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/compiler/parsing/fromSexpScript.sml b/compiler/parsing/fromSexpScript.sml
index 8236b38b24..60c3962fb6 100644
--- a/compiler/parsing/fromSexpScript.sml
+++ b/compiler/parsing/fromSexpScript.sml
@@ -380,7 +380,7 @@ QED
 Theorem strip_sxcons_FAIL_sexplist_FAIL:
    ∀s. (strip_sxcons s = NONE) ⇒ (sexplist p s = NONE)
 Proof
-  Induct >> simp[Once strip_sxcons_def, Once sexplist_def] >>
+  Induct >> simp[Once sexplist_def] >>
   metis_tac[TypeBase.nchotomy_of ``:α option``]
 QED
 
@@ -405,7 +405,7 @@ Theorem strip_sxcons_thm[simp]:
   strip_sxcons (SX_STR str) = NONE ∧
   strip_sxcons (SX_SYM s) = if s = "nil" then SOME [] else NONE
 Proof
-  rpt strip_tac >> simp[Once strip_sxcons_def]
+  rpt strip_tac >> simp[]
 QED
 
 Theorem sexplist_CONG[defncong]: