diff -r 8be65cf94d2e -r d81094515061 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Mon Oct 17 19:19:29 2005 +0200
+++ b/src/FOL/simpdata.ML	Mon Oct 17 23:10:10 2005 +0200
@@ -339,7 +339,7 @@
 
 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*)
@@ -360,7 +360,7 @@
 (*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 ***)