src/FOL/simpdata.ML
changeset 18324 d1c4b1112e33
parent 17892 62c397c17d18
child 18529 540da2415751
--- 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*)