src/FOL/simpdata.ML
changeset 12720 f8a134b9a57f
parent 12526 1b9db2581fe2
child 12725 7ede865e1fe5
     1.1 --- a/src/FOL/simpdata.ML	Fri Jan 11 14:53:05 2002 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Fri Jan 11 14:53:30 2002 +0100
     1.3 @@ -68,8 +68,6 @@
     1.4  
     1.5  (** Conversion into rewrite rules **)
     1.6  
     1.7 -fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
     1.8 -
     1.9  bind_thm ("P_iff_F", int_prove_fun "~P ==> (P <-> False)");
    1.10  bind_thm ("iff_reflection_F", P_iff_F RS iff_reflection);
    1.11  
    1.12 @@ -123,7 +121,7 @@
    1.13           | _ => [th])
    1.14    in atoms end;
    1.15  
    1.16 -fun mksimps pairs = (map mk_eq o mk_atomize pairs o gen_all);
    1.17 +fun mksimps pairs = (map mk_eq o mk_atomize pairs o forall_elim_vars_safe);
    1.18  
    1.19  (*** Classical laws ***)
    1.20