--- a/src/FOL/simpdata.ML Thu Dec 01 18:45:24 2005 +0100
+++ b/src/FOL/simpdata.ML Thu Dec 01 22:03:01 2005 +0100
@@ -338,9 +338,9 @@
setmksimps (mksimps mksimps_pairs)
setmkcong mk_meta_cong;
-fun unfold_tac ss ths =
- ALLGOALS (full_simp_tac
- (Simplifier.inherit_context ss (Simplifier.clear_ss FOL_basic_ss) addsimps ths));
+fun unfold_tac ths =
+ let val ss0 = Simplifier.clear_ss FOL_basic_ss addsimps ths
+ in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
(*intuitionistic simprules only*)