src/HOL/simpdata.ML
changeset 11162 9e2ec5f02217
parent 11034 568eb11f8d52
child 11200 f43fa07536c0
     1.1 --- a/src/HOL/simpdata.ML	Tue Feb 20 13:23:58 2001 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Tue Feb 20 18:47:06 2001 +0100
     1.3 @@ -330,8 +330,6 @@
     1.4    rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the
     1.5    grounds that it allows simplification of R in the two cases.*)
     1.6  
     1.7 -fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
     1.8 -
     1.9  val mksimps_pairs =
    1.10    [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
    1.11     ("All", [spec]), ("True", []), ("False", []),
    1.12 @@ -354,7 +352,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  fun unsafe_solver_tac prems =
    1.20    FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems), atac, etac FalseE];