From a3cf8bbd5a03c4d19450fb325126bd37f2cfffe1 Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Wed, 29 Nov 2023 20:13:45 +0100
Subject: [PATCH] Get a proof to build with an exclude_simps

---
 compiler/repl/evaluate_skipScript.sml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/compiler/repl/evaluate_skipScript.sml b/compiler/repl/evaluate_skipScript.sml
index 8ba3d1b595..f84c0e1f9f 100644
--- a/compiler/repl/evaluate_skipScript.sml
+++ b/compiler/repl/evaluate_skipScript.sml
@@ -341,7 +341,7 @@ Theorem pmatch_update:
           match_res_rel (λenv env'.
             LIST_REL (λ(n,v) (m,w). n = m ∧ v_rel fr ft fe v w)
                      env env') res res')
-Proof
+Proof[exclude_simps = option.OPTREL_NONE]
   ho_match_mp_tac pmatch_ind \\ rw [] \\ gvs [pmatch_def, v_rel_def, SF SFY_ss]
   >- (rw [] \\ gs [])
   >- (