More rebind fixes

CakeML · Oct 16, 2023 · 67dfc72 · 67dfc72
1 parent 81833bf
commit 67dfc72
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 5 deletions.
diff --git a/compiler/repl/evaluate_initScript.sml b/compiler/repl/evaluate_initScript.sml
@@ -682,7 +682,7 @@ Proof
   \\ Cases_on ‘op’ \\ gs []
 QED
 
-Theorem do_app_ok = SIMP_RULE (srw_ss()) [LET_THM] do_app_ok;
+Theorem do_app_ok[allow_rebind] = SIMP_RULE (srw_ss()) [LET_THM] do_app_ok;
 
 Theorem evaluate_ok_Op:
   op ≠ Opapp ∧ op ≠ Eval ⇒ ^(get_goal "App")

diff --git a/translator/okasaki-examples/LazyPairingHeapScript.sml b/translator/okasaki-examples/LazyPairingHeapScript.sml
@@ -112,11 +112,11 @@ decide_tac);
 (* Remove the size constraints *)
 
 val merge_def = SIMP_RULE (srw_ss()) [merge_size_lem, LET_THM] merge_def;
-val _ = save_thm ("merge_def[compute]",merge_def);
+val _ = save_thm ("merge_def[compute,allow_rebind]",merge_def);
 
 val merge_ind =
   SIMP_RULE (srw_ss()) [merge_size_lem, LET_THM] (fetch "-" "merge_ind");
-val _ = save_thm ("merge_ind",merge_ind);
+val _ = save_thm ("merge_ind[allow_rebind]",merge_ind);
 
 val merge_thm = Q.prove(`
   merge get_key leq a b =

diff --git a/translator/other-examples/auxiliary/slr_parser_genScript.sml b/translator/other-examples/auxiliary/slr_parser_genScript.sml
@@ -78,8 +78,6 @@ val addRule = Define `
               if (x = NONE) then NONE
               else SOME (Node l (REVERSE (THE x))))`
 
-val stackSyms = Define `stackSyms stl = (REVERSE (MAP FST (MAP FST stl)))`
-
 val findItemInRules = Define `
   (findItemInRules (item l1 (r1,[])) [] = F) /\
   (findItemInRules (item l1 (r1,[])) ((rule l2 r2)::rst) = T) /\