src/HOL/simpdata.ML
changeset 18324 d1c4b1112e33
parent 18176 ae9bd644d106
child 18407 fa075b606571
--- a/src/HOL/simpdata.ML	Thu Dec 01 18:45:24 2005 +0100
+++ b/src/HOL/simpdata.ML	Thu Dec 01 22:03:01 2005 +0100
@@ -350,9 +350,9 @@
     setmkeqTrue mk_eq_True
     setmkcong mk_meta_cong;
 
-fun unfold_tac ss ths =
-  ALLGOALS (full_simp_tac
-    (Simplifier.inherit_context ss (Simplifier.clear_ss HOL_basic_ss) addsimps ths));
+fun unfold_tac ths =
+  let val ss0 = Simplifier.clear_ss HOL_basic_ss addsimps ths
+  in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
 
 (*In general it seems wrong to add distributive laws by default: they
   might cause exponential blow-up.  But imp_disjL has been in for a while