diff -r beedc794bd67 -r 7ede865e1fe5 src/FOL/simpdata.ML --- a/src/FOL/simpdata.ML Fri Jan 11 18:49:25 2002 +0100 +++ b/src/FOL/simpdata.ML Sat Jan 12 16:37:58 2002 +0100 @@ -121,7 +121,7 @@ | _ => [th]) in atoms end; -fun mksimps pairs = (map mk_eq o mk_atomize pairs o forall_elim_vars_safe); +fun mksimps pairs = (map mk_eq o mk_atomize pairs o gen_all); (*** Classical laws ***)