src/FOL/simpdata.ML

   setmksimps (mksimps mksimps_pairs)
   setmkcong mk_meta_cong;
 
 fun unfold_tac ss ths =
   ALLGOALS (full_simp_tac
-    (Simplifier.inherit_bounds ss (Simplifier.clear_ss FOL_basic_ss) addsimps ths));
+    (Simplifier.inherit_context ss (Simplifier.clear_ss FOL_basic_ss) addsimps ths));
 
 
 (*intuitionistic simprules only*)
 val IFOL_ss = FOL_basic_ss
   addsimps (meta_simps @ IFOL_simps @ int_ex_simps @ int_all_simps)

     "(~P <-> ~Q) <-> (P<->Q)"]);
 
 (*classical simprules too*)
 val FOL_ss = IFOL_ss addsimps (cla_simps @ cla_ex_simps @ cla_all_simps);
 
-val simpsetup = [fn thy => (simpset_ref_of thy := FOL_ss; thy)];
+val simpsetup = [fn thy => (change_simpset_of thy (fn _ => FOL_ss); thy)];
 
 
 (*** integration of simplifier with classical reasoner ***)
 
 structure Clasimp = ClasimpFun