--- a/src/HOL/MicroJava/Comp/CorrComp.thy Mon Oct 17 23:10:10 2005 +0200
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy Mon Oct 17 23:10:13 2005 +0200
@@ -477,7 +477,7 @@
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");
*}
lemma distinct_method: "\<lbrakk> wf_java_prog G; is_class G C;
@@ -1266,7 +1266,7 @@
(* reinstall pair splits *)
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));
*}
declare wf_prog_ws_prog [simp del]