--- a/src/HOL/Bali/DefiniteAssignment.thy Mon Oct 17 23:10:10 2005 +0200
+++ b/src/HOL/Bali/DefiniteAssignment.thy Mon Oct 17 23:10:13 2005 +0200
@@ -830,7 +830,7 @@
declare assigns_if.simps [simp del]
declare split_paired_All [simp del] split_paired_Ex [simp del]
ML_setup {*
-simpset_ref() := simpset() delloop "split_all_tac"
+change_simpset (fn ss => ss delloop "split_all_tac");
*}
inductive_cases da_elim_cases [cases set]:
"Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A"
@@ -897,7 +897,7 @@
declare assigns_if.simps [simp]
declare split_paired_All [simp] split_paired_Ex [simp]
ML_setup {*
-simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
+change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
*}
(* To be able to eliminate both the versions with the overloaded brackets:
(B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A) and with the explicit constructor (B \<guillemotright>In1r Skip\<guillemotright> A),