1.1 --- a/src/HOL/simpdata.ML	Thu Dec 01 18:45:24 2005 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Thu Dec 01 22:03:01 2005 +0100
     1.3 @@ -350,9 +350,9 @@
     1.4      setmkeqTrue mk_eq_True
     1.5      setmkcong mk_meta_cong;
     1.6  
     1.7 -fun unfold_tac ss ths =
     1.8 -  ALLGOALS (full_simp_tac
     1.9 -    (Simplifier.inherit_context ss (Simplifier.clear_ss HOL_basic_ss) addsimps ths));
    1.10 +fun unfold_tac ths =
    1.11 +  let val ss0 = Simplifier.clear_ss HOL_basic_ss addsimps ths
    1.12 +  in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
    1.13  
    1.14  (*In general it seems wrong to add distributive laws by default: they
    1.15    might cause exponential blow-up.  But imp_disjL has been in for a while