From 1cb28eeb9289624b6f187705fe20e6176ccf1406 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 24 Mar 2021 18:11:08 +0000
Subject: Fix lemma for current HOL4 (should also work for older versions)

---
 lib/hol/sail2_valuesAuxiliaryScript.sml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/lib/hol/sail2_valuesAuxiliaryScript.sml b/lib/hol/sail2_valuesAuxiliaryScript.sml
index b475c5ea..d35efacd 100644
--- a/lib/hol/sail2_valuesAuxiliaryScript.sml
+++ b/lib/hol/sail2_valuesAuxiliaryScript.sml
@@ -125,9 +125,8 @@ val just_list_spec = store_thm("just_list_spec",
   conj_tac
   \\ ho_match_mp_tac just_list_ind
   \\ Cases \\ rw[]
-  \\ rw[Once just_list_def]
+  \\ srw_tac [boolSimps.NORMEQ_ss] [Once just_list_def]
   >- ( CASE_TAC \\ fs[] \\ CASE_TAC )
-  >- PROVE_TAC[]
   \\ Cases_on`es` \\ fs[]
   \\ CASE_TAC \\ fs[]
   \\ CASE_TAC \\ fs[]
-- 
cgit v1.2.3