src/HOL/simpdata.ML
changeset 12725 7ede865e1fe5
parent 12524 66eb843b1d35
child 12975 d796a2fd6c69
     1.1 --- a/src/HOL/simpdata.ML	Fri Jan 11 18:49:25 2002 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Sat Jan 12 16:37:58 2002 +0100
     1.3 @@ -221,7 +221,7 @@
     1.4    in atoms end;
     1.5  
     1.6  fun mksimps pairs =
     1.7 -  (mapfilter (try mk_eq) o mk_atomize pairs o forall_elim_vars_safe);
     1.8 +  (mapfilter (try mk_eq) o mk_atomize pairs o gen_all);
     1.9  
    1.10  fun unsafe_solver_tac prems =
    1.11    FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems), atac, etac FalseE];