src/HOLCF/IOA/meta_theory/CompoTraces.ML

 (*  Title:      HOLCF/IOA/meta_theory/CompoTraces.ML
     ID:         $Id$
     Author:     Olaf Müller
 *)
 
-simpset_ref () := simpset() setmksym (K NONE);
+change_simpset (fn ss => ss setmksym (K NONE));
 
 (* ---------------------------------------------------------------- *)
                    section "mksch rewrite rules";
 (* ---------------------------------------------------------------- *)
 

 by (rtac set_ext 1);
 by (asm_full_simp_tac (simpset() addsimps [compositionality_tr,externals_of_par]) 1);
 qed"compositionality_tr_modules";
 
 
-simpset_ref () := simpset() setmksym (SOME o symmetric_fun);
+change_simpset (fn ss => ss setmksym (SOME o symmetric_fun));