--- 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 ***)