replace gen_all by forall_elim_vars_safe;
authorwenzelm
Fri Jan 11 14:53:30 2002 +0100 (2002-01-11 ago)
changeset 12720f8a134b9a57f
parent 12719 41e0d086f8b6
child 12721 226fc0e2e7e3
replace gen_all by forall_elim_vars_safe;
src/FOL/simpdata.ML
src/Sequents/simpdata.ML
src/ZF/Main.ML
src/ZF/OrdQuant.ML
src/ZF/Tools/inductive_package.ML
src/ZF/simpdata.ML
     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  
     2.1 --- a/src/Sequents/simpdata.ML	Fri Jan 11 14:53:05 2002 +0100
     2.2 +++ b/src/Sequents/simpdata.ML	Fri Jan 11 14:53:30 2002 +0100
     2.3 @@ -83,9 +83,6 @@
     2.4  
     2.5  (** Conversion into rewrite rules **)
     2.6  
     2.7 -fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
     2.8 -
     2.9 -
    2.10  (*Make atomic rewrite rules*)
    2.11  fun atomize r =
    2.12   case concl_of r of
    2.13 @@ -243,7 +240,7 @@
    2.14    empty_ss setsubgoaler asm_simp_tac
    2.15      setSSolver (mk_solver "safe" safe_solver)
    2.16      setSolver (mk_solver "unsafe" unsafe_solver)
    2.17 -    setmksimps (map mk_meta_eq o atomize o gen_all)
    2.18 +    setmksimps (map mk_meta_eq o atomize o forall_elim_vars_safe)
    2.19      setmkcong mk_meta_cong;
    2.20  
    2.21  val LK_simps =
     3.1 --- a/src/ZF/Main.ML	Fri Jan 11 14:53:05 2002 +0100
     3.2 +++ b/src/ZF/Main.ML	Fri Jan 11 14:53:30 2002 +0100
     3.3 @@ -4,4 +4,4 @@
     3.4    val thy = the_context ();
     3.5  end;
     3.6  
     3.7 -simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
     3.8 +simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o forall_elim_vars_safe);
     4.1 --- a/src/ZF/OrdQuant.ML	Fri Jan 11 14:53:05 2002 +0100
     4.2 +++ b/src/ZF/OrdQuant.ML	Fri Jan 11 14:53:30 2002 +0100
     4.3 @@ -103,7 +103,7 @@
     4.4  
     4.5  val Ord_atomize = atomize (("OrdQuant.oall", [ospec])::ZF_conn_pairs, ZF_mem_pairs);
     4.6  
     4.7 -simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all)
     4.8 +simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o forall_elim_vars_safe)
     4.9                          addsimps [oall_simp, ltD RS beta]
    4.10                          addcongs [oall_cong, oex_cong, OUN_cong];
    4.11  
     5.1 --- a/src/ZF/Tools/inductive_package.ML	Fri Jan 11 14:53:05 2002 +0100
     5.2 +++ b/src/ZF/Tools/inductive_package.ML	Fri Jan 11 14:53:30 2002 +0100
     5.3 @@ -341,7 +341,7 @@
     5.4       (*We use a MINIMAL simpset. Even FOL_ss contains too many simpules.
     5.5         If the premises get simplified, then the proofs could fail.*)
     5.6       val min_ss = empty_ss
     5.7 -           setmksimps (map mk_eq o ZF_atomize o gen_all)
     5.8 +           setmksimps (map mk_eq o ZF_atomize o forall_elim_vars_safe)
     5.9             setSolver (mk_solver "minimal"
    5.10                        (fn prems => resolve_tac (triv_rls@prems)
    5.11                                     ORELSE' assume_tac
     6.1 --- a/src/ZF/simpdata.ML	Fri Jan 11 14:53:05 2002 +0100
     6.2 +++ b/src/ZF/simpdata.ML	Fri Jan 11 14:53:30 2002 +0100
     6.3 @@ -46,7 +46,7 @@
     6.4  val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
     6.5  
     6.6  simpset_ref() :=
     6.7 -  simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
     6.8 +  simpset() setmksimps (map mk_eq o ZF_atomize o forall_elim_vars_safe)
     6.9    addcongs [if_weak_cong]
    6.10    addsplits [split_if]
    6.11    setSolver (mk_solver "types" (fn prems => TCSET' (fn tcset => type_solver_tac tcset prems)));