src/HOL/MicroJava/Comp/CorrComp.thy

 
 (* to avoid automatic pair splits *)
 
 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; 
   method (G, C) S = Some (D, rT, pns, lvars, blk, res) \<rbrakk> \<Longrightarrow> 
   distinct (gjmb_plns (gmb G C S))"

 
 
 (* 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]
 
 end