diff --git a/examples/algebra/lib/jcLib.sml b/examples/algebra/lib/jcLib.sml
index 6d7062bce5..6286f8ecc5 100644
--- a/examples/algebra/lib/jcLib.sml
+++ b/examples/algebra/lib/jcLib.sml
@@ -19,7 +19,4 @@ fun stripDup ths =
            disch_then (fn th => strip_assume_tac th >>
                                 strip_assume_tac (REWRITE_RULE ths th))]
 
-val _ = Feedback.set_trace "Theory.allow_rebinds" 1
-
-
 end
diff --git a/examples/computability/kolmog/boolListsScript.sml b/examples/computability/kolmog/boolListsScript.sml
index aa7286e767..20c2711424 100644
--- a/examples/computability/kolmog/boolListsScript.sml
+++ b/examples/computability/kolmog/boolListsScript.sml
@@ -1243,7 +1243,7 @@ Proof
        rw[primrec_rules, primrec_pr_nblsnd0, primrec_ell])
 QED
 
-Theorem checkpair_i_def[simp] = new_specification(
+Theorem checkpair_i_def[simp,allow_rebind] = new_specification(
   "checkpair_i_def", ["checkpair_i"],
   MATCH_MP unary_rec_fns_phi recfn_checkpair)
 
diff --git a/examples/computability/kolmog/kraft_ineqScript.sml b/examples/computability/kolmog/kraft_ineqScript.sml
index 90ad731fbf..b9eb86171f 100644
--- a/examples/computability/kolmog/kraft_ineqScript.sml
+++ b/examples/computability/kolmog/kraft_ineqScript.sml
@@ -360,12 +360,12 @@ Proof
   Cases_on‘y=e’>> fsr[] >> RES_TAC >> fsr[]
 QED
 
-Theorem maxr_set_def = new_specification(
+val maxr_set_def = new_specification(
   "maxr_set_def",["maxr_set"],
   SIMP_RULE(srw_ss() )[SKOLEM_THM,GSYM RIGHT_EXISTS_IMP_THM] max_rs_lemma
   );
 
-Theorem minr_set_def = new_specification(
+val minr_set_def = new_specification(
   "minr_set_def",["minr_set"],
   SIMP_RULE(srw_ss() )[SKOLEM_THM,GSYM RIGHT_EXISTS_IMP_THM] min_rs_lemma);
 
diff --git a/examples/computability/turing/turing_machine_primeqScript.sml b/examples/computability/turing/turing_machine_primeqScript.sml
index 2c54dca33b..afeb264cb0 100644
--- a/examples/computability/turing/turing_machine_primeqScript.sml
+++ b/examples/computability/turing/turing_machine_primeqScript.sml
@@ -1200,10 +1200,6 @@ rpt strip_tac >> qexists_tac`Cn (pr2 nel) [proj 0;Cn (pr1 (list_rec_comb c n)) [
 rpt conj_tac >- (rpt (irule primrec_cn >> rw[primrec_rules,primrec_nel,primrec_list_rec_comb]))>>
  simp[list_rec_comb_def] >> simp[list_rec_comb_corr,nel_nlist_of,LIST_REC_def] )
 
-val nleng_thm = new_specification("nleng_def", ["nleng"],
-list_num_rec_thm |> SPECL[``0n``,``Cn succ [proj 2]``]
-                 |> SIMP_RULE (srw_ss())[primrec_cn, primrec_rules])
-
 val nrev_thm = new_specification("nrev_def", ["nrev"],
 list_num_rec_thm |> SPECL[``0n``,``Cn (pr2 napp) [proj 2;Cn (pr2 ncons) [proj 0;zerof] ]``]
                  |> SIMP_RULE (srw_ss())[primrec_cn, primrec_rules])
@@ -1270,12 +1266,6 @@ val primrec_pr_INITIAL_TAPE_TM_NUM = Q.store_thm(
        rw[primrec_rules,primrec_pr_eq,primrec_nsnd,primrec_nfst]) >>
   fs[primrec_proj]);
 
-val pr_INITIAL_TM_NUM_def = Define`
-pr_INITIAL_TM_NUM = Cn (pr2 npair) [zerof;Cn tape_encode
- [Cn (pr1 nfst) [Cn pr_INITIAL_TAPE_TM_NUM [zerof;Cn concatWith_Z [proj 0]]];
-  Cn (pr1 nfst) [Cn (pr1 nsnd) [Cn pr_INITIAL_TAPE_TM_NUM [zerof;Cn concatWith_Z [proj 0]]]];
-  Cn (pr1 nsnd) [Cn (pr1 nsnd) [Cn pr_INITIAL_TAPE_TM_NUM [zerof;Cn concatWith_Z [proj 0]]]]]]`;
-
 val pr_ODD_def = Define`pr_ODD = pr_cond (Cn pr_eq [Cn pr_mod [proj 0;twof];onef]) onef zerof`
 
 val pr_ODD_corr = Q.store_thm("pr_ODD_corr",
@@ -1490,7 +1480,6 @@ Cases_on `A` >> fs[])
 val recfn_rulesl = CONJUNCTS recfn_rules
 val recfnCn = save_thm("recfnCn", List.nth(recfn_rulesl, 3))
 val recfnPr = save_thm("recfnPr", List.nth(recfn_rulesl, 4))
-val recfnMin = save_thm("recfnMin", List.nth(recfn_rulesl, 5))
 
 (* Probably need to include a 'tape reset' type function, ie tm_return_num *)
 val recfn_tm_def = Define`
diff --git a/examples/decidable_separationLogic/src/decidable_separationLogicLibScript.sml b/examples/decidable_separationLogic/src/decidable_separationLogicLibScript.sml
index 18921fc39a..aaafc0eae4 100644
--- a/examples/decidable_separationLogic/src/decidable_separationLogicLibScript.sml
+++ b/examples/decidable_separationLogic/src/decidable_separationLogicLibScript.sml
@@ -1341,47 +1341,23 @@ REPEAT STRIP_TAC THEN (
 
 
 
-val INFERENCE_STAR_INTRODUCTION___EVAL1 = store_thm ("INFERENCE_STAR_INTRODUCTION___EVAL1",
- ``!sfL'' c1 c2 pfL sfL pfL' sfL'.
-         (LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL') ==>
-         LIST_DS_ENTAILS (c1,c2) (pfL,sfL++sfL'') (pfL',sfL'++sfL''))``,
-
-
-REPEAT STRIP_TAC THEN
-`LIST_DS_ENTAILS (c1, c2) (pfL,sfL++sfL'') (pfL',sfL'++sfL'') =
- LIST_DS_ENTAILS (c1, c2) (pfL,sfL''++sfL) (pfL',sfL''++sfL')` by (
-   MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN
-   SIMP_TAC std_ss [PERM_REFL, PERM_APPEND]
-) THEN
-ASM_REWRITE_TAC[] THEN POP_ASSUM (K ALL_TAC) THEN
-
-Induct_on `sfL''` THENL [
-   ASM_SIMP_TAC list_ss [],
-   ASM_SIMP_TAC list_ss [INFERENCE_STAR_INTRODUCTION___IMPL]
-])
-
-
-
-
-val INFERENCE_STAR_INTRODUCTION___EVAL1 = store_thm ("INFERENCE_STAR_INTRODUCTION___EVAL1",
- ``!sfL'' c1 c2 pfL sfL pfL' sfL'.
-         (LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL') ==>
-         LIST_DS_ENTAILS (c1,c2) (pfL,sfL++sfL'') (pfL',sfL'++sfL''))``,
-
-
-REPEAT STRIP_TAC THEN
-`LIST_DS_ENTAILS (c1, c2) (pfL,sfL++sfL'') (pfL',sfL'++sfL'') =
- LIST_DS_ENTAILS (c1, c2) (pfL,sfL''++sfL) (pfL',sfL''++sfL')` by (
-   MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN
-   SIMP_TAC std_ss [PERM_REFL, PERM_APPEND]
-) THEN
-ASM_REWRITE_TAC[] THEN POP_ASSUM (K ALL_TAC) THEN
-
-Induct_on `sfL''` THENL [
+Theorem INFERENCE_STAR_INTRODUCTION___EVAL1:
+ !sfL'' c1 c2 pfL sfL pfL' sfL'.
+   LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL') ==>
+   LIST_DS_ENTAILS (c1,c2) (pfL,sfL++sfL'') (pfL',sfL'++sfL'')
+Proof
+  REPEAT STRIP_TAC THEN
+  ‘LIST_DS_ENTAILS (c1, c2) (pfL,sfL++sfL'') (pfL',sfL'++sfL'') =
+   LIST_DS_ENTAILS (c1, c2) (pfL,sfL''++sfL) (pfL',sfL''++sfL')’
+    by (MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN
+        SIMP_TAC std_ss [PERM_REFL, PERM_APPEND]
+       ) THEN
+  ASM_REWRITE_TAC[] THEN POP_ASSUM (K ALL_TAC) THEN
+  Induct_on ‘sfL''’ THENL [
    ASM_SIMP_TAC list_ss [],
    ASM_SIMP_TAC list_ss [INFERENCE_STAR_INTRODUCTION___IMPL]
-])
-
+  ]
+QED
 
 val INFERENCE_STAR_INTRODUCTION___EVAL2 = store_thm ("INFERENCE_STAR_INTRODUCTION___EVAL2",
  ``!x n1 n2 c1 c2 pfL sfL pfL' sfL'.
diff --git a/examples/formal-languages/regular/regexpScript.sml b/examples/formal-languages/regular/regexpScript.sml
index de0bbfe4b4..7d8766e16e 100644
--- a/examples/formal-languages/regular/regexpScript.sml
+++ b/examples/formal-languages/regular/regexpScript.sml
@@ -130,7 +130,7 @@ Datatype
     | Neg regexp`
 ;
 
-Theorem regexp_induction :
+Theorem regexp_induction[allow_rebind] :
  !P Q.
      (!cs. P (Chset cs)) /\
      (!r r0. P r /\ P r0 ==> P (Cat r r0)) /\
@@ -138,7 +138,7 @@ Theorem regexp_induction :
      (!r. P r ==> P (Neg r)) /\ Q [] /\ (!r l. P r /\ Q l ==> Q (r::l)) ==>
      (!r. P r) /\ !l. Q l
 Proof
- ACCEPT_TAC (fetch "-" "regexp_induction")
+  ACCEPT_TAC (fetch "-" "regexp_induction")
 QED
 
 Triviality regexp_distinct = fetch "-" "regexp_distinct";
diff --git a/examples/fun-op-sem/cbv-lc/logrelScript.sml b/examples/fun-op-sem/cbv-lc/logrelScript.sml
index 91a89c7c63..b24d2c9a8b 100644
--- a/examples/fun-op-sem/cbv-lc/logrelScript.sml
+++ b/examples/fun-op-sem/cbv-lc/logrelScript.sml
@@ -119,7 +119,7 @@ val state_rel_rw =
 Theorem state_rel_rw = state_rel_rw
 
 (* Convert the if-then-else to ⇒ *)
-Theorem val_rel_def = SIMP_RULE (srw_ss()) [] val_rel_def
+Theorem val_rel_def[allow_rebind] = SIMP_RULE (srw_ss()) [] val_rel_def
 
 (* Package up exec_rel nicely in terms of res_rel. *)
 Theorem exec_rel_rw:
diff --git a/examples/fun-op-sem/ml/typeSoundScript.sml b/examples/fun-op-sem/ml/typeSoundScript.sml
index 66ce8cd7ad..92ce125975 100644
--- a/examples/fun-op-sem/ml/typeSoundScript.sml
+++ b/examples/fun-op-sem/ml/typeSoundScript.sml
@@ -280,8 +280,9 @@ val sem_clock = store_thm("sem_clock",
 val r = term_rewrite [``check_clock s1 s = s1``,
     ``s.clock <> 0 /\ s1.clock <> 0 <=> s1.clock <> 0``]
 
-val sem_def = store_thm("sem_def",
-  sem_def |> concl |> r,
+Theorem sem_def[allow_rebind]:
+  ^(sem_def |> concl |> r)
+Proof
   rpt strip_tac >>
   rw[Once sem_def] >>
   BasicProvers.CASE_TAC >>
@@ -294,10 +295,12 @@ val sem_def = store_thm("sem_def",
   imp_res_tac sem_clock >>
   simp[check_clock_id] >>
   `F` suffices_by rw[] >>
-  DECIDE_TAC)
+  DECIDE_TAC
+QED
 
-val sem_ind = store_thm("sem_ind",
-  sem_ind |> concl |> r,
+Theorem sem_ind[allow_rebind]:
+  ^(sem_ind |> concl |> r)
+Proof
   ntac 2 strip_tac >>
   ho_match_mp_tac sem_ind >>
   rw[] >>
@@ -306,7 +309,8 @@ val sem_ind = store_thm("sem_ind",
   res_tac >>
   imp_res_tac sem_clock >>
   fsrw_tac[ARITH_ss][check_clock_id] >> rfs[] >>
-  fsrw_tac[ARITH_ss][check_clock_id])
+  fsrw_tac[ARITH_ss][check_clock_id]
+QED
 
 (* alternative un-clocked relational big-step semantics for comparison *)
 
diff --git a/examples/l3-machine-code/arm/decompiler/arm_decomp_demoScript.sml b/examples/l3-machine-code/arm/decompiler/arm_decomp_demoScript.sml
index 9b97c667e0..f8cec66256 100644
--- a/examples/l3-machine-code/arm/decompiler/arm_decomp_demoScript.sml
+++ b/examples/l3-machine-code/arm/decompiler/arm_decomp_demoScript.sml
@@ -283,7 +283,6 @@ val (PID_C2_cert, PID_C2_def) = core_decompilerLib.core_decompile "PID_C2" `
     edc37a00             (* vstr       s15, [r3]                *)
     e8bd0010             (* pop        {r4}                     *)`;
 
-val _ = save_thm("PID_C2_def",PID_C2_def);
 val _ = save_thm("PID_C2_cert",PID_C2_cert);
 
 val () = export_theory()
diff --git a/examples/l3-machine-code/m0/step/m0_stepScript.sml b/examples/l3-machine-code/m0/step/m0_stepScript.sml
index 747e25877f..5464668cab 100644
--- a/examples/l3-machine-code/m0/step/m0_stepScript.sml
+++ b/examples/l3-machine-code/m0/step/m0_stepScript.sml
@@ -741,13 +741,6 @@ val Decode_simps = save_thm("Decode_simps",
                      blastLib.BBLAST_CONV ``v2w [a; b; c] = ^w``
                   end)) |> Drule.LIST_CONJ);
 
-val Shift_C_LSL_rwt = Q.store_thm("Shift_C_LSL_rwt",
-   `!imm2 w C s.
-        Shift_C (w: word32, SRType_LSL, imm2, C) s =
-        ((w << imm2, if imm2 = 0 then C else testbit 32 (shiftl (w2v w) imm2)),
-         s)`,
-   lrw [Shift_C_def, LSL_C_def, bitstringTheory.shiftl_replicate_F])
-
 local
    val lem =
     (SIMP_RULE (srw_ss()) [] o Q.SPECL [`v`, `32`] o
diff --git a/examples/l3-machine-code/x64/decompiler/x64_decomp_demoScript.sml b/examples/l3-machine-code/x64/decompiler/x64_decomp_demoScript.sml
index cbc2b72bc1..a745d118f6 100644
--- a/examples/l3-machine-code/x64/decompiler/x64_decomp_demoScript.sml
+++ b/examples/l3-machine-code/x64/decompiler/x64_decomp_demoScript.sml
@@ -38,7 +38,10 @@ val _ = save_thm("decomp_cert",decomp_cert);
 
 val () = Feedback.set_trace "x64 spec" 2
 
-val (decomp1_cert,decomp1_def) = x64_decompLib.x64_decompile "decomp1" `
+val (decomp1_cert,decomp1_def) =
+  Feedback.trace ("Theory.allow_rebinds", 1)
+     (x64_decompLib.x64_decompile "decomp1")
+  ‘
   (*  0: *) 55              (* push   %rbp *)
   (*  1: *) 4889e5          (* mov    %rsp,%rbp *)
   (*  4: *) 4883ec20        (* sub    $0x20,%rsp *)
@@ -62,7 +65,7 @@ val (decomp1_cert,decomp1_def) = x64_decompLib.x64_decompile "decomp1" `
   (* 3b: *) 84c0            (* test   %al,%al *)
   (* 3d: *) 75d7            (* jne    16 <transform+0x16> *)
   (* 3f: *) 488b45e8        (* mov    -0x18(%rbp),%rax *)
-  (* 43: *) c9              (* leaveq  *) `
+  (* 43: *) c9              (* leaveq  *) ’
 
 val _ = save_thm("decomp1_cert",decomp1_cert);
 
diff --git a/examples/lambda/Holmakefile b/examples/lambda/Holmakefile
index 9f81933e08..89d3c3e996 100644
--- a/examples/lambda/Holmakefile
+++ b/examples/lambda/Holmakefile
@@ -1,2 +1,2 @@
 CLINE_OPTIONS = -r
-INCLUDES = barendregt basics other-models typing wcbv-reasonable
+INCLUDES = barendregt basics other-models typing wcbv-reasonable examples
diff --git a/examples/lambda/examples/holScript.sml b/examples/lambda/examples/holScript.sml
index 7643219aa8..591375ad4d 100644
--- a/examples/lambda/examples/holScript.sml
+++ b/examples/lambda/examples/holScript.sml
@@ -6,16 +6,15 @@ open basic_swapTheory nomsetTheory NEWLib
 
 val _ = new_theory "hol"
 
-fun Store_thm (n,t,tac) = store_thm(n,t,tac) before export_rewrites [n]
-
 (* a theory of higher order logic terms, as modelled in systems such as
    HOL4, Isabelle/HOL and HOL Light *)
 
 (* HOL types *)
 
-val _ = Hol_datatype `hol_type = tyvar of string
-                               | tyop of string => hol_type list
-`
+Datatype:
+  hol_type = tyvar string
+           | tyop string (hol_type list)
+End
 
 
 (*
@@ -26,18 +25,20 @@ it has to be
 
 *)
 
-val _ = Hol_datatype`raw_holterm = rhvar of string # hol_type
-                                 | rhconst of string # hol_type
-                                 | rhapp of raw_holterm => raw_holterm
-                                 | rhabs of string # hol_type => raw_holterm
-`
+
+Datatype:
+  raw_holterm = rhvar (string # hol_type)
+              | rhconst (string # hol_type)
+              | rhapp raw_holterm raw_holterm
+              | rhabs (string # hol_type) raw_holterm
+End
 
 (* but what is the appropriate notion of permutation on this type?
 
    It seems clear that it has to be the permutation of atoms that consist of
    names coupled with types *)
 
-val rawpm_def = Define`
+Definition rawpm_def[simp]:
   (rawpm ty pi (rhvar nty) = if ty = SND nty then
                                rhvar (lswapstr pi (FST nty), SND nty)
                              else rhvar nty) /\
@@ -47,125 +48,110 @@ val rawpm_def = Define`
      rhabs (if ty = SND nty then (lswapstr pi (FST nty), SND nty)
             else nty)
            (rawpm ty pi t))
-`;
-val _ = export_rewrites ["rawpm_def"]
-
-val rawpm_is_perm = Store_thm(
-  "rawpm_is_perm",
-  ``!ty. is_perm (rawpm ty)``,
-  SRW_TAC [][is_perm_def] THENL [
-    Induct_on `x` THEN SRW_TAC [][],
-    Induct_on `x` THEN SRW_TAC [][lswapstr_APPEND] THEN
-    FULL_SIMP_TAC (srw_ss()) [],
-    FULL_SIMP_TAC (srw_ss()) [permeq_def, FUN_EQ_THM] THEN
-    Induct THEN SRW_TAC [][]
-  ]);
-
-val rawpms_differing_types_commute = store_thm(
-  "rawpms_differing_types_commute",
-  ``~(ty1 = ty2) ==>
-    (rawpm ty1 pi1 (rawpm ty2 pi2 t) =
-     rawpm ty2 pi2 (rawpm ty1 pi1 t))``,
-  Induct_on `t` THEN SRW_TAC [][] THEN METIS_TAC [])
-
-val rawpm_nil = Store_thm(
-  "rawpm_nil",
-  ``rawpm ty [] t = t``,
-  METIS_TAC [is_perm_nil, rawpm_is_perm]);
-
-val rawpm_APPEND = store_thm(
-  "rawpm_APPEND",
-  ``rawpm ty p1 (rawpm ty p2 t) = rawpm ty (p1 ++ p2) t``,
-  METIS_TAC [rawpm_is_perm, is_perm_decompose]);
-
-val rawpm_inverse = Store_thm(
-  "rawpm_inverse",
-  ``(rawpm ty pi (rawpm ty (REVERSE pi) t) = t) /\
-    (rawpm ty (REVERSE pi) (rawpm ty pi t) = t)``,
-  METIS_TAC [rawpm_is_perm, is_perm_inverse]);
-
-val rawpm_sing_inv = Store_thm(
-  "rawpm_sing_inv",
-  ``(rawpm ty [h] (rawpm ty [h] x) = x)``,
-  METIS_TAC [rawpm_is_perm, is_perm_sing_inv]);
-
-val rawpm_sing_to_back = store_thm(
-  "rawpm_sing_to_back",
-  ``rawpm ty [(lswapstr pi a, lswapstr pi b)] (rawpm ty pi t) =
-    rawpm ty pi (rawpm ty [(a,b)] t)``,
-  METIS_TAC [rawpm_is_perm, is_perm_sing_to_back]);
-
-val allvars_def = Define`
+End
+
+Theorem rawpm_is_perm:
+  !ty. is_pmact (rawpm ty)
+Proof
+  SRW_TAC [][is_pmact_def]
+  >- (Induct_on `x` THEN SRW_TAC [][])
+  >- (Induct_on `x` >> rw[pmact_decompose] >> gvs[]) >>
+  simp[FUN_EQ_THM] >> Induct >> rw[] >>
+  metis_tac[pmact_permeq]
+QED
+
+Overload rhpmact = “λty. mk_pmact (rawpm ty)”
+Overload rhpm = “λty. pmact (rhpmact ty)”
+
+Theorem rawpm_rhpm:
+  rawpm ty = rhpm ty
+Proof
+  simp[GSYM pmact_bijections, rawpm_is_perm]
+QED
+
+Theorem rhpm_thm[simp] = ONCE_REWRITE_RULE [rawpm_rhpm] rawpm_def
+
+Theorem rawpms_differing_types_commute:
+  ty1 ≠ ty2 ==>
+  rhpm ty1 pi1 (rhpm ty2 pi2 t) = rhpm ty2 pi2 (rhpm ty1 pi1 t)
+Proof
+  Induct_on `t` THEN SRW_TAC [][] THEN METIS_TAC []
+QED
+
+Definition allvars_def[simp]:
   (allvars ty (rhvar nty) = if ty = SND nty then {FST nty} else {}) /\
   (allvars ty (rhconst nty) = {}) /\
   (allvars ty (rhapp t1 t2) = allvars ty t1 UNION allvars ty t2) /\
   (allvars ty (rhabs nty t) = (if ty = SND nty then {FST nty} else {}) UNION
                               allvars ty t)
-`;
-val _ = export_rewrites ["allvars_def"]
-
-val IN_allvars_rawpm = Store_thm(
-  "IN_allvars_rawpm",
-  ``x IN allvars ty (rawpm ty pi t) =
-    lswapstr (REVERSE pi) x IN allvars ty t``,
-  Induct_on `t` THEN SRW_TAC [][lswapstr_eql] THEN
-  FULL_SIMP_TAC (srw_ss()) []);
-
-val allvars_rawpm_diff = Store_thm(
-  "allvars_rawpm_diff",
-  ``~(ty1 = ty2) ==> (allvars ty1 (rawpm ty2 pi t) = allvars ty1 t)``,
-  Induct_on `t` THEN SRW_TAC [][] THEN METIS_TAC []);
-
-val FINITE_allvars = Store_thm(
-  "FINITE_allvars",
-  ``FINITE (allvars ty t)``,
-  Induct_on `t` THEN SRW_TAC [][]);
-
-val allvars_fresh = store_thm(
-  "allvars_fresh",
-  ``~(u IN allvars ty t) /\ ~(v IN allvars ty t) ==>
-    (rawpm ty [(u,v)] t = t)``,
-  Induct_on `t` THEN SRW_TAC [][]);
-
-val (aeq_rules, aeq_ind, aeq_cases) = Hol_reln`
+End
+
+Theorem IN_allvars_rawpm[simp]:
+  x IN allvars ty (rhpm ty pi t) <=>
+  lswapstr (REVERSE pi) x IN allvars ty t
+Proof
+  Induct_on `t` >> simp[] >> rw[] >> SRW_TAC [][pmact_eql] >> gs[]
+QED
+
+Theorem allvars_rawpm_diff[simp]:
+  ty1 ≠ ty2 ==> allvars ty1 (rhpm ty2 pi t) = allvars ty1 t
+Proof
+  Induct_on `t` THEN SRW_TAC [][] THEN METIS_TAC []
+QED
+
+Theorem FINITE_allvars[simp]:
+  FINITE (allvars ty t)
+Proof
+  Induct_on `t` THEN SRW_TAC [][]
+QED
+
+Theorem allvars_fresh:
+  u ∉ allvars ty t ∧ v ∉ allvars ty t ⇒ rhpm ty [(u,v)] t = t
+Proof
+  Induct_on `t` THEN SRW_TAC [][]
+QED
+
+Inductive aeq:
+[~var:]
   (!v. aeq (rhvar v) (rhvar v)) /\
+[~const:]
   (!v. aeq (rhconst v) (rhconst v)) /\
+[~app:]
   (!t1 t2 u1 u2. aeq t1 u1 /\ aeq t2 u2 ==>
                  aeq (rhapp t1 t2) (rhapp u1 u2)) /\
-  (!v1 v2 u t z.
+[~lam:]
+  (!v1 v2 u t z ty.
       ~(z IN allvars ty t) /\ ~(z IN allvars ty u) /\ ~(z = v1) /\
-      ~(z = v2) /\ aeq (rawpm ty [(z,v1)] t) (rawpm ty [(z,v2)] u) ==>
+      ~(z = v2) /\ aeq (rhpm ty [(z,v1)] t) (rhpm ty [(z,v2)] u) ==>
       aeq (rhabs (v1,ty) t) (rhabs (v2,ty) u))
-`;
+End
 
-val aeq_rawpm = store_thm(
-  "aeq_rawpm",
-  ``!t u. aeq t u ==> !pi ty. aeq (rawpm ty pi t) (rawpm ty pi u)``,
+Theorem aeq_rawpm:
+  !t u. aeq t u ==> !pi ty. aeq (rhpm ty pi t) (rhpm ty pi u)
+Proof
   HO_MATCH_MP_TAC aeq_ind THEN SRW_TAC [][aeq_rules] THEN
-  Cases_on `ty = ty'` THENL [
-    SRW_TAC [][] THEN
-    MATCH_MP_TAC (last (CONJUNCTS aeq_rules)) THEN
-    Q.EXISTS_TAC `lswapstr pi z` THEN SRW_TAC [][] THEN
-    SRW_TAC [][is_perm_sing_to_back, rawpm_is_perm],
-    SRW_TAC [][] THEN
-    MATCH_MP_TAC (last (CONJUNCTS aeq_rules)) THEN
-    SRW_TAC [][] THEN
-    METIS_TAC [rawpms_differing_types_commute]
-  ]);
-
-val aeq_rawpml = store_thm(
-  "aeq_rawpml",
-  ``aeq (rawpm ty pi t1) t2 = aeq t1 (rawpm ty (REVERSE pi) t2)``,
-  METIS_TAC [rawpm_inverse, aeq_rawpm]);
-
-val aeq_refl = Store_thm(
-  "aeq_refl",
-  ``aeq t t``,
+  Cases_on `ty = ty'`
+  >- (rw[] >> irule aeq_lam >>
+      qexists ‘lswapstr pi z’ >> rw[pmact_sing_to_back]) >>
+  rw[] >> irule aeq_lam >> rw[] >>
+  metis_tac [rawpms_differing_types_commute]
+QED
+
+Theorem aeq_rawpml:
+  aeq (rhpm ty pi t1) t2 = aeq t1 (rhpm ty (REVERSE pi) t2)
+Proof
+  METIS_TAC [pmact_inverse, aeq_rawpm]
+QED
+
+Theorem aeq_refl[simp]:
+  aeq t t
+Proof
   Induct_on `t` THEN SRW_TAC [][aeq_rules] THEN
   Cases_on `p` THEN
   Q_TAC (NEW_TAC "z") `q INSERT allvars r t` THEN
-  MATCH_MP_TAC (last (CONJUNCTS aeq_rules)) THEN
-  Q.EXISTS_TAC `z` THEN SRW_TAC [][aeq_rawpm]);
+  MATCH_MP_TAC aeq_lam THEN
+  Q.EXISTS_TAC `z` THEN SRW_TAC [][aeq_rawpm]
+QED
 
 val aeq_sym = store_thm(
   "aeq_sym",
@@ -173,19 +159,18 @@ val aeq_sym = store_thm(
   HO_MATCH_MP_TAC aeq_ind THEN SRW_TAC [][aeq_rules] THEN
   METIS_TAC [aeq_rules]);
 
-val aeq_app = store_thm(
-  "aeq_app",
+val aeq_app_rwt = store_thm(
+  "aeq_app_rwt",
   ``aeq (rhapp t u) z = ?z1 z2. (z = rhapp z1 z2) /\
                                 aeq t z1 /\ aeq u z2``,
   CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [aeq_cases])) THEN
   SRW_TAC [][]);
 
-val aeq_trans = store_thm(
-  "aeq_trans",
-  ``!s t u. aeq s t /\ aeq t u ==> aeq s u``,
-  Q_TAC SUFF_TAC `!s t. aeq s t ==> !u. aeq t u ==> aeq s u`
-        THEN1 METIS_TAC [] THEN
-  HO_MATCH_MP_TAC aeq_ind THEN SRW_TAC [][aeq_rules, aeq_app] THEN
+Theorem aeq_trans:
+  !s t u. aeq s t /\ aeq t u ==> aeq s u
+Proof
+  Induct_on ‘aeq’ >>
+  rw[aeq_rules, aeq_app_rwt] >>
   POP_ASSUM MP_TAC THEN
   CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [aeq_cases])) THEN
   SIMP_TAC (srw_ss()) [] THEN
@@ -195,58 +180,57 @@ val aeq_trans = store_thm(
   SRW_TAC [][] THEN
   Q_TAC (NEW_TAC "d") `{v;v1;v2;z;z'} UNION allvars ty t UNION
                        allvars ty u UNION allvars ty s` THEN
-  `!u'. aeq (rawpm ty [(d,z)] (rawpm ty [(z,v2)] u))
-            (rawpm ty [(d,z)] u') ==>
-        aeq (rawpm ty [(d,z)] (rawpm ty [(z,v1)] t))
-            (rawpm ty [(d,z)] u')`
+  ‘!u'. aeq (rhpm ty [(d,z)] (rhpm ty [(z,v2)] u))
+            (rhpm ty [(d,z)] u') ==>
+        aeq (rhpm ty [(d,z)] (rhpm ty [(z,v1)] t))
+            (rhpm ty [(d,z)] u')’
       by SRW_TAC [][aeq_rawpml] THEN
-  POP_ASSUM (Q.SPEC_THEN `rawpm ty [(d,z)] u'`
+  POP_ASSUM (Q.SPEC_THEN `rhpm ty [(d,z)] u'`
              (ASSUME_TAC o Q.GEN `u'` o
               SIMP_RULE (srw_ss()) [])) THEN
   POP_ASSUM (MP_TAC o
-             ONCE_REWRITE_RULE [GSYM rawpm_sing_to_back]) THEN
+             ONCE_REWRITE_RULE [GSYM pmact_sing_to_back]) THEN
   SRW_TAC [][allvars_fresh] THEN
-  `aeq (rawpm ty [(d,z')] (rawpm ty [(z',v2)] u))
-       (rawpm ty [(d,z')] (rawpm ty [(z',v)] s))`
+  ‘aeq (rhpm ty [(d,z')] (rhpm ty [(z',v2)] u))
+       (rhpm ty [(d,z')] (rhpm ty [(z',v)] s))’
      by SRW_TAC [][Once aeq_rawpml] THEN
-  POP_ASSUM (MP_TAC o ONCE_REWRITE_RULE [GSYM rawpm_sing_to_back]) THEN
-  SRW_TAC [][allvars_fresh, swapstr_def] THEN
-  METIS_TAC [aeq_rules]);
+  POP_ASSUM (MP_TAC o ONCE_REWRITE_RULE [GSYM pmact_sing_to_back]) THEN
+  SRW_TAC [][allvars_fresh] THEN
+  METIS_TAC [aeq_rules]
+QED
 
-val fv_def = Define`
+Definition fv_def[simp]:
   (fv ty (rhvar nty) = if ty = SND nty then {FST nty} else {}) /\
   (fv ty (rhconst nty) = {}) /\
   (fv ty (rhapp t1 t2) = fv ty t1 UNION fv ty t2) /\
   (fv ty (rhabs nty t) =
        if ty = SND nty then fv ty t DELETE FST nty
        else fv ty t)
-`;
-val _ = export_rewrites ["fv_def"]
+End
 
-val fv_SUBSET_allvars = store_thm(
-  "fv_SUBSET_allvars",
-  ``!x. x IN fv ty t ==> x IN allvars ty t``,
-  Induct_on `t` THEN SRW_TAC [][] THEN SRW_TAC [][]);
+Theorem fv_SUBSET_allvars:
+  !x. x IN fv ty t ==> x IN allvars ty t
+Proof
+  Induct_on `t` THEN SRW_TAC [][] THEN SRW_TAC [][]
+QED
 
 val IN_fv_rawpm = store_thm(
   "IN_fv_rawpm",
-  ``x IN fv ty (rawpm ty pi t) = lswapstr (REVERSE pi) x IN fv ty t``,
-  Induct_on `t` THEN SRW_TAC [][lswapstr_eql] THEN
+  ``x IN fv ty (rhpm ty pi t) ⇔ lswapstr (REVERSE pi) x IN fv ty t``,
+  Induct_on `t` THEN SRW_TAC [][pmact_eql] THEN
   FULL_SIMP_TAC (srw_ss()) []);
 
 val fv_rawpm_diff = store_thm(
   "fv_rawpm_diff",
-  ``~(ty = ty') ==> (fv ty (rawpm ty' pi t) = fv ty t)``,
+  ``~(ty = ty') ==> (fv ty (rhpm ty' pi t) = fv ty t)``,
   Induct_on `t` THEN SRW_TAC [][] THEN METIS_TAC []);
 
-
-val aeq_fv = store_thm(
-  "aeq_fv",
-  ``!t u. aeq t u ==> !ty. fv ty t = fv ty u``,
+Theorem aeq_fv:
+  !t u. aeq t u ==> !ty. fv ty t = fv ty u
+Proof
   HO_MATCH_MP_TAC aeq_ind THEN SRW_TAC [][EXTENSION] THEN
   COND_CASES_TAC THENL [
     SRW_TAC [][] THEN
-    SRW_TAC [][EXTENSION] THEN
     POP_ASSUM (Q.SPEC_THEN `ty` MP_TAC) THEN
     Cases_on `x = v1` THENL [
       SRW_TAC [][] THEN
@@ -265,29 +249,32 @@ val aeq_fv = store_thm(
     ],
     SRW_TAC [][] THEN FIRST_X_ASSUM (Q.SPEC_THEN `ty'` MP_TAC) THEN
     SRW_TAC [][fv_rawpm_diff]
-  ]);
+  ]
+QED
 
-val rhabs_respects_aeq = store_thm(
-  "rhabs_respects_aeq",
-  ``!t u. aeq t u ==> aeq (rhabs v t) (rhabs v u)``,
+Theorem rhabs_respects_aeq:
+  !t u. aeq t u ==> aeq (rhabs v t) (rhabs v u)
+Proof
   SRW_TAC [][] THEN Cases_on `v` THEN
   MATCH_MP_TAC (last (CONJUNCTS aeq_rules)) THEN
   Q_TAC (NEW_TAC "z") `q INSERT allvars r t UNION allvars r u` THEN
-  SRW_TAC [][aeq_rawpml] THEN METIS_TAC []);
-
-val alt_aeq_lam = store_thm(
-  "alt_aeq_lam",
-  ``(!z. ~(z IN allvars ty t1) /\ ~(z IN allvars ty t2) /\ ~(z = u) /\
-         ~(z = v) ==>
-         aeq (rawpm ty [(u,z)] t1) (rawpm ty [(v,z)] t2)) ==>
-    aeq (rhabs (u,ty) t1) (rhabs (v,ty) t2)``,
+  SRW_TAC [][aeq_rawpml] THEN METIS_TAC []
+QED
+
+Theorem alt_aeq_lam:
+  (!z. ~(z IN allvars ty t1) /\ ~(z IN allvars ty t2) /\ ~(z = u) /\
+       ~(z = v) ==>
+       aeq (rhpm ty [(u,z)] t1) (rhpm ty [(v,z)] t2)) ==>
+  aeq (rhabs (u,ty) t1) (rhabs (v,ty) t2)
+Proof
   STRIP_TAC THEN MATCH_MP_TAC (last (CONJUNCTS aeq_rules)) THEN
   Q_TAC (NEW_TAC "z") `allvars ty t1 UNION allvars ty t2 UNION {u;v}` THEN
-  METIS_TAC [rawpm_is_perm, is_perm_flip_args]);
+  METIS_TAC [rawpm_is_perm, pmact_flip_args]
+QED
 
-val fresh_swap = store_thm(
-  "fresh_swap",
-  ``!x y. ~(x IN fv ty t) /\ ~(y IN fv ty t) ==> aeq t (rawpm ty [(x,y)] t)``,
+Theorem fresh_swap:
+  !x y. x ∉ fv ty t ∧ y ∉ fv ty t ⇒ aeq t (rhpm ty [(x,y)] t)
+Proof
   Induct_on `t` THEN
   ASM_SIMP_TAC (srw_ss()) [aeq_rules, pairTheory.FORALL_PROD] THEN1
     SRW_TAC [][] THEN
@@ -299,30 +286,31 @@ val fresh_swap = store_thm(
     REPEAT STRIP_TAC THEN
     `~(z IN fv p_2 t)` by METIS_TAC [fv_SUBSET_allvars] THEN
     Cases_on `x = p_1` THEN ASM_SIMP_TAC (srw_ss()) [] THENL [
-      FULL_SIMP_TAC (srw_ss()) [is_perm_id] THEN
+      FULL_SIMP_TAC (srw_ss()) [pmact_id] THEN
       SRW_TAC [][] THEN
       Cases_on `y = p_1` THEN SRW_TAC [][] THEN
       CONV_TAC (RAND_CONV (RAND_CONV (ONCE_REWRITE_CONV
-                                        [GSYM rawpm_sing_to_back]))) THEN
+                                        [GSYM pmact_sing_to_back]))) THEN
       SRW_TAC [][],
       ALL_TAC
     ] THEN
     Cases_on `y = p_1` THEN SRW_TAC [][] THENL [
       FULL_SIMP_TAC (srw_ss()) [] THEN
       CONV_TAC (RAND_CONV (RAND_CONV (ONCE_REWRITE_CONV
-                                        [GSYM rawpm_sing_to_back]))) THEN
-      SRW_TAC [][is_perm_flip_args, rawpm_is_perm],
+                                        [GSYM pmact_sing_to_back]))) THEN
+      SRW_TAC [][pmact_flip_args],
       SRW_TAC [][]
     ],
     SRW_TAC [][rhabs_respects_aeq]
-  ]);
-
-val aeq_lam_eqn = store_thm(
-  "aeq_lam_eqn",
-  ``(aeq (rhabs (n1,ty1) t1) (rhabs (n2,ty2) t2)) =
-      (ty1 = ty2) /\
-      ((n1 = n2) /\ aeq t1 t2 \/
-       ~(n1 = n2) /\ ~(n1 IN fv ty1 t2) /\ aeq t1 (rawpm ty1 [(n1,n2)] t2))``,
+  ]
+QED
+
+Theorem aeq_lam_eqn:
+  aeq (rhabs (n1,ty1) t1) (rhabs (n2,ty2) t2) ⇔
+    ty1 = ty2 ∧
+    (n1 = n2 ∧ aeq t1 t2 \/
+     n1 ≠ n2 ∧ n1 ∉ fv ty1 t2 ∧ aeq t1 (rhpm ty1 [(n1,n2)] t2))
+Proof
   SIMP_TAC (srw_ss()) [EQ_IMP_THM, DISJ_IMP_THM] THEN REPEAT CONJ_TAC THENL [
     CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [aeq_cases])) THEN
     SRW_TAC [][] THEN
@@ -331,31 +319,31 @@ val aeq_lam_eqn = store_thm(
     Cases_on `n1 = n2` THEN1 FULL_SIMP_TAC (srw_ss()) [aeq_rawpml] THEN
     `~(n1 IN fv ty1 t2)`
        by (STRIP_TAC THEN
-           `n1 IN fv ty1 (rawpm ty1 [(z,n2)] t2)`
+           `n1 IN fv ty1 (rhpm ty1 [(z,n2)] t2)`
               by SRW_TAC [][IN_fv_rawpm] THEN
-           `n1 IN fv ty1 (rawpm ty1 [(z,n1)] t1)` by METIS_TAC [aeq_fv] THEN
+           `n1 IN fv ty1 (rhpm ty1 [(z,n1)] t1)` by METIS_TAC [aeq_fv] THEN
            FULL_SIMP_TAC (srw_ss()) [IN_fv_rawpm]) THEN
     FULL_SIMP_TAC (srw_ss()) [aeq_rawpml] THEN
-    Q.PAT_ASSUM `aeq X Y` MP_TAC THEN
-    ONCE_REWRITE_TAC [GSYM rawpm_sing_to_back] THEN
+    Q.PAT_X_ASSUM `aeq X Y` MP_TAC THEN
+    ONCE_REWRITE_TAC [GSYM pmact_sing_to_back] THEN
     SRW_TAC [][] THEN
     MATCH_MP_TAC aeq_trans THEN
-    Q.EXISTS_TAC `rawpm ty1 [(n1,n2)] (rawpm ty1 [(z,n1)] t2)` THEN
+    Q.EXISTS_TAC `rhpm ty1 [(n1,n2)] (rhpm ty1 [(z,n1)] t2)` THEN
     SRW_TAC [][] THEN
     SRW_TAC [][aeq_rawpml, fresh_swap],
 
     SRW_TAC [][] THENL [
       SRW_TAC [][rhabs_respects_aeq],
       MATCH_MP_TAC alt_aeq_lam THEN SRW_TAC [][aeq_rawpml] THEN
-      ONCE_REWRITE_TAC [GSYM rawpm_sing_to_back] THEN
+      ONCE_REWRITE_TAC [GSYM pmact_sing_to_back] THEN
       SRW_TAC [][] THEN
       `~(z IN fv ty1 t2)` by METIS_TAC [fv_SUBSET_allvars] THEN
       MATCH_MP_TAC aeq_trans THEN
-      Q.EXISTS_TAC `rawpm ty1 [(n1,n2)] t2` THEN SRW_TAC [][] THEN
-      SRW_TAC [][is_perm_flip_args, rawpm_is_perm, fresh_swap,
-                 aeq_rawpml]
+      Q.EXISTS_TAC `rhpm ty1 [(n1,n2)] t2` THEN SRW_TAC [][] THEN
+      SRW_TAC [][pmact_flip_args, fresh_swap, aeq_rawpml]
     ]
-  ]);
+  ]
+QED
 
 val aeq_equiv = prove(
   ``!t1 t2. aeq t1 t2 = (aeq t1 = aeq t2)``,
@@ -388,18 +376,20 @@ val aeq_fv' = prove(
                     (fv ty1 t1 = fv ty2 t2)``,
   SRW_TAC [][aeq_fv]);
 
-val aeq_rawpm' = prove(
+val aeq_rawpm0 = prove(
   ``!ty1 ty2 pi1 pi2 t u.
         (ty1 = ty2) /\ (pi1 = pi2) /\ aeq t u ==>
-        aeq (rawpm ty1 pi1 t) (rawpm ty2 pi2 u)``,
+        aeq (rhpm ty1 pi1 t) (rhpm ty2 pi2 u)``,
   SRW_TAC [][aeq_rawpm]);
 
-val [FV_thm, simple_induction, FINITE_FV, tpm_thm] =
+val aeq_rawpm' = SRULE [GSYM rawpm_rhpm] aeq_rawpm0
+
+val [FV_thm, simple_induction, FINITE_FV, raw_tpm_thm(*, tpm_is_pmact*)] =
     quotient.define_quotient_types_full {
       types = [{name = "term", equiv = aeq_equiv}],
       defs = map mk_def [("LAM", ``rhabs``), ("COMB", ``rhapp``),
                          ("VAR", ``rhvar``), ("CONST", ``rhconst``),
-                         ("FV", ``fv``), ("tpm", ``rawpm``)],
+                         ("FV", ``fv``), ("raw_tpm", ``rawpm``)],
       tyop_equivs = [],
       tyop_quotients = [],
       tyop_simps = [],
@@ -408,29 +398,27 @@ val [FV_thm, simple_induction, FINITE_FV, tpm_thm] =
       respects = [rhabs_respects, List.nth(CONJUNCTS aeq_rules, 2),
                   aeq_fv', aeq_rawpm', var_respects, con_respects],
       old_thms = [fv_def, TypeBase.induction_of ``:raw_holterm``,
-                  finite_fv, rawpm_def]
+                  finite_fv, rawpm_def(*, rawpm_is_perm*)]
 }
 
-val FV_thm = save_thm("FV_thm", FV_thm)
-val _ = export_rewrites ["FV_thm"]
-val simple_induction = save_thm("simple_induction", simple_induction)
-val FINITE_FV = save_thm("FINITE_FV", FINITE_FV)
-val _ = export_rewrites ["FINITE_FV"]
-val tpm_thm = save_thm("tpm_thm", tpm_thm)
-val _ = export_rewrites ["tpm_thm"]
-
-val tpm_is_perm = Store_thm(
-  "tpm_is_perm",
-  ``is_perm (tpm ty)``,
-  SRW_TAC [][is_perm_def] THENL [
+Theorem FV_thm[simp] = FV_thm
+Theorem simple_induction = simple_induction
+Theorem FINITE_FV[simp] = FINITE_FV
+Theorem raw_tpm_thm[simp] = raw_tpm_thm
+
+Theorem tpm_is_perm:
+  is_pmact (raw_tpm ty)
+Proof
+  SRW_TAC [][is_pmact_def] THENL [
     Q.ID_SPEC_TAC `x` THEN HO_MATCH_MP_TAC simple_induction THEN
     SRW_TAC [][],
     Q.ID_SPEC_TAC `x` THEN HO_MATCH_MP_TAC simple_induction THEN
-    SRW_TAC [][lswapstr_APPEND] THEN SRW_TAC [][] THEN
-    FULL_SIMP_TAC (srw_ss()) [],
-    FULL_SIMP_TAC (srw_ss()) [FUN_EQ_THM, permeq_def] THEN
-    HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][]
-  ]);
+    SRW_TAC [][pmact_decompose] THEN SRW_TAC [][] THEN
+    gs[],
+    simp[FUN_EQ_THM] >> Induct using simple_induction >>
+    SRW_TAC [][] >> metis_tac[pmact_permeq]
+  ]
+QED
 
 val _ = export_theory()
 
diff --git a/examples/machine-code/decompiler/decompilerLib.sml b/examples/machine-code/decompiler/decompilerLib.sml
index 6d3fee66c6..fae6e430c7 100644
--- a/examples/machine-code/decompiler/decompilerLib.sml
+++ b/examples/machine-code/decompiler/decompilerLib.sml
@@ -1642,7 +1642,7 @@ fun extract_function name th entry exit function_in_out = let
   val main_thm = finalise main_thm
   val pre_thm = finalise pre_thm
   (* define temporary abbreviation *)
-  val silly_string = Theory.temp_binding "(( step ))"
+  val silly_string = Theory.temp_binding "((step))"
   val step_def =
      new_definition
         (silly_string,mk_eq(mk_var(silly_string,type_of step_fun),step_fun))
diff --git a/examples/separationLogic/src/generalHelpersScript.sml b/examples/separationLogic/src/generalHelpersScript.sml
index c7c555d9e0..b8fa5e8141 100644
--- a/examples/separationLogic/src/generalHelpersScript.sml
+++ b/examples/separationLogic/src/generalHelpersScript.sml
@@ -113,36 +113,12 @@ val EL_LUPDATE___NO_COND = store_thm ("EL_LUPDATE___NO_COND",
 SIMP_TAC std_ss [EL_LUPDATE]);
 
 
-val TAKE_LUPDATE = store_thm ("TAKE_LUPDATE",
-``!n1 n2 e l. TAKE n1 (LUPDATE e n2 l) =
-  if (n1 <= n2) then TAKE n1 l else
-  LUPDATE e n2 (TAKE n1 l)``,
-
-Induct_on `n1` THEN
-Cases_on `n2` THEN
-Cases_on `l` THEN
-ASM_SIMP_TAC list_ss [LUPDATE_def,
-  COND_RAND, COND_RATOR])
-
-
 val TAKE_LUPDATE___SIMPLE = store_thm ("TAKE_LUPDATE___SIMPLE",
 ``!n1 n2 e l. TAKE n1 (LUPDATE e n2 l) =
   LUPDATE e n2 (TAKE n1 l)``,
 Induct_on `n1` THEN Cases_on `n2` THEN Cases_on `l` THEN
 ASM_SIMP_TAC list_ss [LUPDATE_def])
 
-
-val DROP_LUPDATE = store_thm ("DROP_LUPDATE",
-``!n1 n2 e l. DROP n1 (LUPDATE e n2 l) =
-   if (n2 < n1) then DROP n1 l else
-  LUPDATE e (n2-n1) (DROP n1 l)``,
-
-Induct_on `n1` THEN
-Cases_on `n2` THEN
-Cases_on `l` THEN
-ASM_SIMP_TAC list_ss [LUPDATE_def]);
-
-
 val LUPDATE_APPEND1 = store_thm ("LUPDATE_APPEND1",
 ``!n l1 l2. n < LENGTH l1 ==> (
      LUPDATE e n (l1 ++ l2) =
@@ -1059,10 +1035,6 @@ val IMAGE_ABS2 = store_thm ("IMAGE_ABS2",
 ``IMAGE f P = (\x. ?y. (x = f y) /\ y IN P)``,
 SIMP_TAC std_ss [EXTENSION, IN_IMAGE, IN_ABS]);
 
-val IMAGE_ABS = store_thm ("IMAGE_ABS",
-``IMAGE f (\x. P x) = (\x. ?y. (x = f y) /\ P y)``,
-SIMP_TAC std_ss [IMAGE_ABS2, IN_ABS]);
-
 val IN_ABS2 = store_thm ("IN_ABS2",
         ``(!t. (t IN X = Q t)) = (X = \t. Q t)``,
 SIMP_TAC std_ss [EXTENSION, IN_ABS]);
diff --git a/examples/temporal_deep/src/deep_embeddings/ctl_starScript.sml b/examples/temporal_deep/src/deep_embeddings/ctl_starScript.sml
index e432e90422..dd8fb95195 100644
--- a/examples/temporal_deep/src/deep_embeddings/ctl_starScript.sml
+++ b/examples/temporal_deep/src/deep_embeddings/ctl_starScript.sml
@@ -441,39 +441,6 @@ val LTL_TO_CTL_STAR_def =
    (LTL_TO_CTL_STAR (LTL_PSUNTIL (f1, f2)) = (CTL_STAR_PSUNTIL (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2)))`;
 
 
-val LTL_TO_CTL_STAR_THM =
-  store_thm ("LTL_TO_CTL_STAR_THM",
-    ``!b f c f1 f2.
-   (LTL_TO_CTL_STAR (LTL_PROP b) = (CTL_STAR_PROP b)) /\
-   (LTL_TO_CTL_STAR (LTL_NOT f) = (CTL_STAR_NOT (LTL_TO_CTL_STAR f))) /\
-   (LTL_TO_CTL_STAR (LTL_AND (f1, f2)) = (CTL_STAR_AND (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_OR (f1, f2)) = (CTL_STAR_OR (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_IMPL (f1, f2)) = (CTL_STAR_IMPL (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_COND (c, f1, f2)) = (CTL_STAR_COND (LTL_TO_CTL_STAR c, LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_EQUIV (f1, f2)) = (CTL_STAR_EQUIV (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_NEXT f) = (CTL_STAR_NEXT (LTL_TO_CTL_STAR f))) /\
-   (LTL_TO_CTL_STAR (LTL_EVENTUAL f) = (CTL_STAR_EVENTUAL (LTL_TO_CTL_STAR f))) /\
-   (LTL_TO_CTL_STAR (LTL_ALWAYS f) = (CTL_STAR_ALWAYS (LTL_TO_CTL_STAR f))) /\
-   (LTL_TO_CTL_STAR (LTL_SUNTIL (f1, f2)) = (CTL_STAR_SUNTIL (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_UNTIL (f1, f2)) = (CTL_STAR_UNTIL (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_BEFORE (f1, f2)) = (CTL_STAR_BEFORE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_SBEFORE (f1, f2)) = (CTL_STAR_SBEFORE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_WHILE (f1, f2)) = (CTL_STAR_WHILE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_SWHILE (f1, f2)) = (CTL_STAR_SWHILE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_PSNEXT f) = (CTL_STAR_PSNEXT (LTL_TO_CTL_STAR f))) /\
-   (LTL_TO_CTL_STAR (LTL_PNEXT f) = (CTL_STAR_PNEXT (LTL_TO_CTL_STAR f))) /\
-   (LTL_TO_CTL_STAR (LTL_PEVENTUAL f) = (CTL_STAR_PEVENTUAL (LTL_TO_CTL_STAR f))) /\
-   (LTL_TO_CTL_STAR (LTL_PALWAYS f) = (CTL_STAR_PALWAYS (LTL_TO_CTL_STAR f))) /\
-   (LTL_TO_CTL_STAR (LTL_PSUNTIL (f1, f2)) = (CTL_STAR_PSUNTIL (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_PUNTIL (f1, f2)) = (CTL_STAR_PUNTIL (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_PBEFORE (f1, f2)) = (CTL_STAR_PBEFORE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_PSBEFORE (f1, f2)) = (CTL_STAR_PSBEFORE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_PWHILE (f1, f2)) = (CTL_STAR_PWHILE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_PSWHILE (f1, f2)) = (CTL_STAR_PSWHILE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2)))``,
-
-   EVAL_TAC THEN PROVE_TAC[]);
-
-
 val LTL_FORMULAS_ARE_PATH_FORMULAS =
   store_thm (
     "LTL_FORMULAS_ARE_PATH_FORMULAS",
diff --git a/examples/temporal_deep/src/deep_embeddings/infinite_pathScript.sml b/examples/temporal_deep/src/deep_embeddings/infinite_pathScript.sml
index 79a052da9a..1cc3b9739f 100644
--- a/examples/temporal_deep/src/deep_embeddings/infinite_pathScript.sml
+++ b/examples/temporal_deep/src/deep_embeddings/infinite_pathScript.sml
@@ -403,35 +403,6 @@ val BEFORE_ON_PATH_STRONG___BEFORE_ON_PATH =
    EXISTS_TAC ``u:num`` THEN
    FULL_SIMP_TAC arith_ss []);
 
-
-val BEFORE_ON_PATH___SUC =
- store_thm
-  ("BEFORE_ON_PATH___SUC",
-   ``!v t a b. ((BEFORE_ON_PATH_RESTN t v a b) /\ ~(P_SEM (v t) a)) ==> (BEFORE_ON_PATH_RESTN (SUC t) v a b)``,
-   REWRITE_TAC [BEFORE_ON_PATH_RESTN_def] THEN
-   REPEAT STRIP_TAC THEN
-   `t <= t'` by DECIDE_TAC THEN
-   RES_TAC THEN
-   EXISTS_TAC ``u:num`` THEN
-   ASM_REWRITE_TAC[] THEN
-   `~(u = t)` by METIS_TAC[] THEN
-   DECIDE_TAC);
-
-
-val BEFORE_ON_PATH_STRONG___SUC =
- store_thm
-  ("BEFORE_ON_PATH_STRONG___SUC",
-   ``!v t a b. ((BEFORE_ON_PATH_RESTN_STRONG t v a b) /\ ~(P_SEM (v t) a)) ==> (BEFORE_ON_PATH_RESTN_STRONG (SUC t) v a b)``,
-   REWRITE_TAC [BEFORE_ON_PATH_RESTN_STRONG_def] THEN
-   REPEAT STRIP_TAC THEN
-   `t <= t'` by DECIDE_TAC THEN
-   RES_TAC THEN
-   EXISTS_TAC ``u:num`` THEN
-   ASM_REWRITE_TAC[] THEN
-   `~(u = t)` by METIS_TAC[] THEN
-   DECIDE_TAC);
-
-
 val NOT_ON_PATH___IMP_ON_PATH =
  store_thm
   ("NOT_ON_PATH___IMP_ON_PATH",
diff --git a/examples/temporal_deep/src/deep_embeddings/kripke_structureScript.sml b/examples/temporal_deep/src/deep_embeddings/kripke_structureScript.sml
index f781a53c80..e81648ae36 100644
--- a/examples/temporal_deep/src/deep_embeddings/kripke_structureScript.sml
+++ b/examples/temporal_deep/src/deep_embeddings/kripke_structureScript.sml
@@ -357,17 +357,6 @@ val IS_TOTAL_COMPLETELY_REACHABLE_KRIPKE_STRUCTURE___ALTERNATIVE_DEF =
   ]);
 
 
-
-
-val IS_WELL_FORMED_KRIPKE_STRUCTURE_def =
- Define
-  `IS_WELL_FORMED_KRIPKE_STRUCTURE K =
-    (FINITE K.S /\ FINITE K.P /\ K.S0 SUBSET K.S /\
-     K.R SUBSET (K.S CROSS K.S) /\
-     (!s. (s IN K.S) ==> (K.L s) SUBSET K.P))`
-
-
-
 val LANGUAGE_OF_KRIPKE_STRUCTURE_def =
  Define
   `LANGUAGE_OF_KRIPKE_STRUCTURE K  =
@@ -730,41 +719,22 @@ REPEAT STRIP_TAC THENL [
 ]);
 
 
-
-val PRODUCT_KRIPKE_STRUCTURES___PATH_IS_PRODUCT_OF_ORIGINAL_PATHS =
-  store_thm (
-    "PRODUCT_KRIPKE_STRUCTURES___PATH_IS_PRODUCT_OF_ORIGINAL_PATHS",
-
-   ``!K1 K2 p. IS_PATH_THROUGH_KRIPKE_STRUCTURE (PRODUCT_KRIPKE_STRUCTURE K1 K2) p ==>
-               (IS_PATH_THROUGH_KRIPKE_STRUCTURE K1 (\n. FST (p n)) /\
-                IS_PATH_THROUGH_KRIPKE_STRUCTURE K2 (\n. SND (p n)))``,
-
-    SIMP_TAC std_ss [IS_PATH_THROUGH_KRIPKE_STRUCTURE_def,
-      PRODUCT_KRIPKE_STRUCTURE_def, kripke_structure_REWRITES,
-      GSPECIFICATION] THEN
-    REPEAT STRIP_TAC THEN (
-      SPECL_NO_ASSUM 0 [``n:num``] THEN
-      SIMP_ALL_TAC std_ss [] THEN
-      Cases_on `x` THEN Cases_on `r` THEN Cases_on `r'` THEN
-      FULL_SIMP_TAC std_ss []
-    ));
-
-
-val PRODUCT_KRIPKE_STRUCTURES___PATH_IS_PRODUCT_OF_ORIGINAL_PATHS =
-  store_thm (
-    "PRODUCT_KRIPKE_STRUCTURES___PATH_IS_PRODUCT_OF_ORIGINAL_PATHS",
-
-   ``!K1 K2 p. IS_PATH_THROUGH_KRIPKE_STRUCTURE (PRODUCT_KRIPKE_STRUCTURE K1 K2) p =
-               (IS_PATH_THROUGH_KRIPKE_STRUCTURE K1 (\n. FST (p n)) /\
-                IS_PATH_THROUGH_KRIPKE_STRUCTURE K2 (\n. SND (p n)) /\
-                (!n. (K1.L (FST (p n)) INTER K1.P INTER K2.P =
-                      K2.L (SND (p n)) INTER K1.P INTER K2.P)))``,
-
-    SIMP_TAC std_ss [IS_PATH_THROUGH_KRIPKE_STRUCTURE_def,
-      PRODUCT_KRIPKE_STRUCTURE_def, kripke_structure_REWRITES,
-      GSPECIFICATION, FORALL_PROD, EXISTS_PROD] THEN
-    SIMP_TAC std_ss [prove (``!x y1 y2. (x = (y1, y2)) = ((FST x = y1) /\ (SND x = y2))``, Cases_on `x` THEN SIMP_TAC std_ss []), FORALL_AND_THM] THEN
-    REPEAT STRIP_TAC THEN REPEAT BOOL_EQ_STRIP_TAC);
+Theorem PRODUCT_KRIPKE_STRUCTURES___PATH_IS_PRODUCT_OF_ORIGINAL_PATHS:
+  !K1 K2 p.
+    IS_PATH_THROUGH_KRIPKE_STRUCTURE (PRODUCT_KRIPKE_STRUCTURE K1 K2) p =
+    (IS_PATH_THROUGH_KRIPKE_STRUCTURE K1 (\n. FST (p n)) /\
+     IS_PATH_THROUGH_KRIPKE_STRUCTURE K2 (\n. SND (p n)) /\
+     (!n. (K1.L (FST (p n)) INTER K1.P INTER K2.P =
+           K2.L (SND (p n)) INTER K1.P INTER K2.P)))
+Proof
+  SIMP_TAC std_ss [IS_PATH_THROUGH_KRIPKE_STRUCTURE_def,
+                   PRODUCT_KRIPKE_STRUCTURE_def, kripke_structure_REWRITES,
+                   GSPECIFICATION, FORALL_PROD, EXISTS_PROD] THEN
+  SIMP_TAC std_ss [
+    prove (“!x y1 y2. (x = (y1, y2)) = ((FST x = y1) /\ (SND x = y2))”,
+           Cases_on `x` THEN SIMP_TAC std_ss []), FORALL_AND_THM] THEN
+  REPEAT STRIP_TAC THEN REPEAT BOOL_EQ_STRIP_TAC
+QED
 
 
 (*open model*)
diff --git a/examples/temporal_deep/src/tools/set_lemmataScript.sml b/examples/temporal_deep/src/tools/set_lemmataScript.sml
index d11cdfc3b7..f8952d7568 100644
--- a/examples/temporal_deep/src/tools/set_lemmataScript.sml
+++ b/examples/temporal_deep/src/tools/set_lemmataScript.sml
@@ -280,45 +280,6 @@ val IMAGE_ID_SUBSET =
    SIMP_TAC std_ss [IMAGE_DEF, EXTENSION, GSPECIFICATION] THEN
    METIS_TAC[]);
 
-
-
-val UNION_INSERT =
- store_thm
-  ("UNION_INSERT",
-   ``!S1 S2 a. (S1 UNION (a INSERT S2)) = ((a INSERT S1) UNION S2)``,
-
-SIMP_TAC std_ss [UNION_DEF, INSERT_DEF, EXTENSION, GSPECIFICATION] THEN
-PROVE_TAC[]);
-
-
-val UNION_INTER_ABSORPTION =
- store_thm
-  ("UNION_INTER_ABSORPTION",
-   ``!s1 s2. (((s1 UNION s2) INTER s1) = s1) /\ ((s1 UNION (s2 INTER s1)) = s1)``,
-
-   REPEAT STRIP_TAC THEN
-   REWRITE_TAC [UNION_DEF, INTER_DEF, EXTENSION, GSPECIFICATION] THEN
-   FULL_SIMP_TAC arith_ss [] THEN
-   PROVE_TAC[]);
-
-
-val INTER_INTER_ABSORPTION =
- store_thm
-  ("INTER_INTER_ABSORPTION",
-    ``!S a. S INTER a INTER a = S INTER a``,
-
-       PROVE_TAC[INTER_SUBSET, SUBSET_INTER_ABSORPTION]
-);
-
-val SUBSET_COMPL_DISJOINT =
- store_thm
-  ("SUBSET_COMPL_DISJOINT",
-   ``!s1 s2. (s1 SUBSET (COMPL s2)) = (DISJOINT s1 s2)``,
-
-   SIMP_TAC arith_ss [SUBSET_DEF, COMPL_DEF, DISJOINT_DEF, INTER_DEF, DIFF_DEF, IN_UNIV, GSPECIFICATION, EXTENSION, NOT_IN_EMPTY] THEN
-   PROVE_TAC[]
-);
-
 val INJ_SUBSET_DOMAIN =
  store_thm
   ("INJ_SUBSET_DOMAIN",
diff --git a/src/TeX/theory_tests/Holmakefile b/src/TeX/theory_tests/Holmakefile
index 2a3f11554f..58dbdd84ec 100644
--- a/src/TeX/theory_tests/Holmakefile
+++ b/src/TeX/theory_tests/Holmakefile
@@ -57,4 +57,6 @@ dupop20171208: dupop20171208_input dupop20171208_expected munge_d20171208.exe
 
 .PHONY: all check_output check_utyabb_output check_tyabb_output check_gh242 dupop20171208
 
-EXTRA_CLEANS = munge.exe tymunge.exe utymunge.exe output utyabb_output tyabb_output gh242_output dupop20171208_output
+EXTRA_CLEANS = \
+  munge.exe tymunge.exe utymunge.exe munge_d20171208.exe munge248.exe \
+  output utyabb_output tyabb_output gh242_output dupop20171208_output
diff --git a/src/coalgebras/itreeTauScript.sml b/src/coalgebras/itreeTauScript.sml
index ab5b550984..054f3326f5 100644
--- a/src/coalgebras/itreeTauScript.sml
+++ b/src/coalgebras/itreeTauScript.sml
@@ -511,7 +511,7 @@ Theorem itree_bisimulation:
     ?R. R t1 t2 /\
         (!x t. R (Ret x) t ==> t = Ret x) /\
         (!u t. R (Tau u) t ==> ?v. t = Tau v /\ R u v) /\
-        (!a f t. R (Vis a f) t ==> ?b g. t = Vis a g /\ !s. R (f s) (g s))
+        (!a f t. R (Vis a f) t ==> ?g. t = Vis a g /\ !s. R (f s) (g s))
 Proof
   rw [] \\ eq_tac \\ rw []
   THEN1 (qexists_tac ‘(=)’ \\ fs [itree_11])
@@ -568,6 +568,8 @@ val _ = TypeBase.export
       destructors = [],
       recognizers = [] } ]
 
+Overload "case" = “itree_CASE”
+
 (* itree combinators *)
 
 Definition itree_bind_def:
@@ -580,7 +582,7 @@ Definition itree_bind_def:
                   Ret s =>
                     Ret' s
                 | Tau t =>
-                    Tau'(INR t)
+                    Tau' (INR t)
                 | Vis e g =>
                      Vis' e (INR o g))
            | INL(Vis e g) => Vis' e (INL o g)
@@ -802,7 +804,7 @@ Theorem itree_wbisim_strong_coind:
        (?t2 t3. t = Tau t2 /\ t' = Tau t3 /\ (R t2 t3 \/ itree_wbisim t2 t3)) \/
        (?e k k'.
           strip_tau t (Vis e k) /\ strip_tau t' (Vis e k') /\
-          !r. R (k r) (k' r) \/ itree_wbisim(k r) (k' r)) \/
+          !r. R (k r) (k' r) \/ itree_wbisim (k r) (k' r)) \/
        ?r. strip_tau t (Ret r) /\ strip_tau t' (Ret r)) ==>
     !t t'. R t t' ==> itree_wbisim t t'
 Proof
@@ -818,6 +820,38 @@ Proof
   metis_tac[]
 QED
 
+Triviality itree_wbisim_coind_upto_equiv:
+  !R t t'.
+    itree_wbisim t t' ==>
+    (?t2 t3. t = Tau t2 /\ t' = Tau t3 /\ (R t2 t3 \/ itree_wbisim t2 t3)) \/
+    (?e k k'.
+       strip_tau t (Vis e k) /\ strip_tau t' (Vis e k') /\
+       !r. R (k r) (k' r) \/ itree_wbisim (k r) (k' r)) \/
+    ?r. strip_tau t (Ret r) /\ strip_tau t' (Ret r)
+Proof
+  metis_tac[itree_wbisim_cases]
+QED
+
+Theorem itree_wbisim_coind_upto:
+  !R.
+    (!t t'.
+       R t t' ==>
+       (?t2 t3. t = Tau t2 /\ t' = Tau t3 /\ (R t2 t3 \/ itree_wbisim t2 t3)) \/
+       (?e k k'.
+          strip_tau t (Vis e k) /\ strip_tau t' (Vis e k') /\
+          !r. R (k r) (k' r) \/ itree_wbisim (k r) (k' r)) \/
+       (?r. strip_tau t (Ret r) /\ strip_tau t' (Ret r))
+       \/ itree_wbisim t t')
+    ==> !t t'. R t t' ==> itree_wbisim t t'
+Proof
+  rpt strip_tac >>
+  irule itree_wbisim_strong_coind >>
+  qexists_tac ‘R’ >>
+  fs[] >>
+  pop_assum kall_tac >>
+  metis_tac[itree_wbisim_coind_upto_equiv]
+QED
+
 Theorem itree_wbisim_tau:
   !t t'. itree_wbisim (Tau t) t' ==> itree_wbisim t t'
 Proof
@@ -898,6 +932,100 @@ Proof
             itree_wbisim_sym]
 QED
 
+Theorem itree_bind_wbisim_tau_eq[simp]:
+  !x k y. itree_wbisim (itree_bind (Tau x) k) y <=> itree_wbisim (itree_bind x k) y
+Proof
+  metis_tac[itree_bind_thm, itree_wbisim_tau_eq,
+            itree_wbisim_sym, itree_wbisim_trans]
+QED
+
+Theorem itree_bind_strip_tau_wbisim:
+  !u u' k. strip_tau u u' ==> itree_wbisim (itree_bind u k) (itree_bind u' k)
+Proof
+  Induct_on ‘strip_tau’ >>
+  rpt strip_tac >> rw[itree_wbisim_refl]
+QED
+
+(* note a similar theorem does NOT hold for Ret because bind expands to (k x) *)
+Theorem itree_bind_vis_strip_tau:
+  !u k k' e. strip_tau u (Vis e k') ==>
+             strip_tau (itree_bind u k) (Vis e (λx. itree_bind (k' x) k))
+Proof
+  strip_tac >> strip_tac >> strip_tac >> strip_tac >>
+  Induct_on ‘strip_tau’ >>
+  rpt strip_tac >>
+  rw[itree_bind_thm]
+QED
+
+Triviality itree_bind_vis_tau_wbisim:
+  itree_wbisim (Vis a g) (Tau u) ==>
+  ?e k' k''.
+    strip_tau (itree_bind (Vis a g) k) (Vis e k') /\
+    strip_tau (itree_bind (Tau u) k) (Vis e k'') /\
+    !r. (?t1 t2. itree_wbisim t1 t2 /\
+                 k' r = itree_bind t1 k /\ k'' r = itree_bind t2 k) \/
+        itree_wbisim (k' r) (k'' r)
+Proof
+  rpt strip_tac >>
+  fs[Once itree_wbisim_cases, itree_bind_thm] >>
+  fs[Once $ GSYM itree_wbisim_cases] >>
+  qexists_tac ‘λx. itree_bind (k' x) k’ >>
+  rw[itree_bind_vis_strip_tau] >>
+  metis_tac[]
+QED
+
+Theorem itree_bind_resp_t_wbisim:
+  !a b k. itree_wbisim a b ==> itree_wbisim (itree_bind a k) (itree_bind b k)
+Proof
+  rpt strip_tac >>
+  qspecl_then [‘λa b. ?t1 t2. itree_wbisim t1 t2 /\
+                              a = itree_bind t1 k /\ b = itree_bind t2 k’]
+              strip_assume_tac itree_wbisim_coind_upto >>
+  pop_assum irule >>
+  rw[] >-
+   (last_x_assum kall_tac >>
+    Cases_on ‘t1’ >>
+    Cases_on ‘t2’ >-
+     (fs[Once itree_wbisim_cases, itree_bind_thm] >>
+      Cases_on ‘k x’ >> rw[itree_wbisim_refl]) >-
+     (disj2_tac >> disj2_tac >> disj2_tac >>
+      irule itree_wbisim_sym >>
+      irule itree_bind_strip_tau_wbisim >>
+      fs[Once itree_wbisim_cases]) >-
+     (fs[Once itree_wbisim_cases]) >-
+     (disj2_tac >> disj2_tac >> disj2_tac >>
+      irule itree_bind_strip_tau_wbisim >>
+      fs[Once itree_wbisim_cases]) >-
+     (rw[itree_bind_thm] >>
+      ‘itree_wbisim u u'’ by metis_tac[itree_wbisim_tau, itree_wbisim_sym] >>
+      metis_tac[]) >-
+     (metis_tac[itree_wbisim_sym, itree_bind_vis_tau_wbisim]) >-
+     (fs[Once itree_wbisim_cases]) >-
+     (metis_tac[itree_wbisim_sym, itree_bind_vis_tau_wbisim]) >-
+     (fs[itree_bind_thm, Once itree_wbisim_cases] >> metis_tac[]))
+  >- metis_tac[]
+QED
+
+Theorem itree_bind_resp_k_wbisim:
+  !t k1 k2. (!r. itree_wbisim (k1 r) (k2 r)) ==>
+            itree_wbisim (itree_bind t k1) (itree_bind t k2)
+Proof
+  rpt strip_tac >>
+  qspecl_then [‘λa b. ?t. a = itree_bind t k1 /\ b = itree_bind t k2’]
+              strip_assume_tac itree_wbisim_coind_upto >>
+  pop_assum irule >>
+  rw[] >-
+   (Cases_on ‘t''’ >> rw[itree_bind_thm] >> metis_tac[]) >-
+   metis_tac[]
+QED
+
+Theorem itree_bind_resp_wbisim:
+  !a b k1 k2. itree_wbisim a b /\ (!r. itree_wbisim (k1 r) (k2 r)) ==>
+              itree_wbisim (itree_bind a k1) (itree_bind b k2)
+Proof
+  metis_tac[itree_bind_resp_t_wbisim, itree_bind_resp_k_wbisim, itree_wbisim_trans]
+QED
+
 (* misc *)
 
 Definition spin:
diff --git a/src/postkernel/Theory.sml b/src/postkernel/Theory.sml
index 11db89b935..499efc42ed 100644
--- a/src/postkernel/Theory.sml
+++ b/src/postkernel/Theory.sml
@@ -393,9 +393,12 @@ fun add_term {name,theory,htype} thy =
     (Term.prim_new_const {Thy = theory, Name = name} htype; thy)
 
 fun add_fact th (seg : segment) =
-    let val updator = if !Globals.interactive orelse !allow_rebinds then
-                        Symtab.update
-                      else Symtab.update_new
+    let val updator =
+            if !Globals.interactive orelse !allow_rebinds orelse
+               is_temp_binding (#1 th)
+            then
+              Symtab.update
+            else Symtab.update_new
     in
       update_seg seg (U #facts (updator th (#facts seg))) $$
     end