# HG changeset patch
# User wenzelm
# Date 1010849878 -3600
# Node ID 7ede865e1fe5069dee3de86256a5711bcdc46a9f
# Parent  beedc794bd670c0d09291daa3347cace77887096
renamed forall_elim_vars_safe to gen_all;

diff -r beedc794bd67 -r 7ede865e1fe5 doc-src/Ref/simplifier.tex
--- a/doc-src/Ref/simplifier.tex	Fri Jan 11 18:49:25 2002 +0100
+++ b/doc-src/Ref/simplifier.tex	Sat Jan 12 16:37:58 2002 +0100
@@ -1335,7 +1335,7 @@
 automatically.  Preprocessing involves extracting atomic rewrites at the
 object-level, then reflecting them to the meta-level.
 
-To start, the function \texttt{forall_elim_vars_safe} strips any meta-level
+To start, the function \texttt{gen_all} strips any meta-level
 quantifiers from the front of the given theorem.
 
 The function \texttt{atomize} analyses a theorem in order to extract
@@ -1398,7 +1398,7 @@
   | _                           => th RS iff_reflection_T;
 \end{ttbox}
 The 
-three functions \texttt{forall_elim_vars_safe}, \texttt{atomize} and \texttt{mk_eq} 
+three functions \texttt{gen_all}, \texttt{atomize} and \texttt{mk_eq} 
 will be composed together and supplied below to \texttt{setmksimps}.
 
 
@@ -1427,7 +1427,7 @@
 %
 The basic simpset for intuitionistic FOL is \ttindexbold{FOL_basic_ss}.  It
 preprocess rewrites using 
-{\tt forall_elim_vars_safe}, \texttt{atomize} and \texttt{mk_eq}.
+{\tt gen_all}, \texttt{atomize} and \texttt{mk_eq}.
 It solves simplified subgoals using \texttt{triv_rls} and assumptions, and by
 detecting contradictions.  It uses \ttindex{asm_simp_tac} to tackle subgoals
 of conditional rewrites.
@@ -1451,7 +1451,7 @@
                addsimprocs [defALL_regroup, defEX_regroup]
                setSSolver   safe_solver
                setSolver  unsafe_solver
-               setmksimps (map mk_eq o atomize o forall_elim_vars_safe)
+               setmksimps (map mk_eq o atomize o gen_all)
                setmkcong mk_meta_cong;
 
 val IFOL_ss = 
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 ***)
 
diff -r beedc794bd67 -r 7ede865e1fe5 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Fri Jan 11 18:49:25 2002 +0100
+++ b/src/HOL/simpdata.ML	Sat Jan 12 16:37:58 2002 +0100
@@ -221,7 +221,7 @@
   in atoms end;
 
 fun mksimps pairs =
-  (mapfilter (try mk_eq) o mk_atomize pairs o forall_elim_vars_safe);
+  (mapfilter (try mk_eq) o mk_atomize pairs o gen_all);
 
 fun unsafe_solver_tac prems =
   FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems), atac, etac FalseE];
diff -r beedc794bd67 -r 7ede865e1fe5 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Fri Jan 11 18:49:25 2002 +0100
+++ b/src/Pure/Isar/object_logic.ML	Sat Jan 12 16:37:58 2002 +0100
@@ -139,7 +139,7 @@
 
 fun gen_rulify full thm =
   Tactic.simplify full (get_rulify (Thm.sign_of_thm thm)) thm
-  |> Drule.forall_elim_vars_safe |> Drule.strip_shyps_warning |> Drule.zero_var_indexes;
+  |> Drule.gen_all |> Drule.strip_shyps_warning |> Drule.zero_var_indexes;
 
 val rulify = gen_rulify true;
 val rulify_no_asm = gen_rulify false;
diff -r beedc794bd67 -r 7ede865e1fe5 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Jan 11 18:49:25 2002 +0100
+++ b/src/Pure/drule.ML	Sat Jan 12 16:37:58 2002 +0100
@@ -31,7 +31,7 @@
   val forall_elim_list  : cterm list -> thm -> thm
   val forall_elim_var   : int -> thm -> thm
   val forall_elim_vars  : int -> thm -> thm
-  val forall_elim_vars_safe  : thm -> thm
+  val gen_all           : thm -> thm
   val freeze_thaw       : thm -> thm * (thm -> thm)
   val implies_elim_list : thm -> thm list -> thm
   val implies_intr_list : cterm list -> thm -> thm
@@ -315,7 +315,7 @@
 val forall_elim_var = PureThy.forall_elim_var;
 val forall_elim_vars = PureThy.forall_elim_vars;
 
-fun forall_elim_vars_safe thm =
+fun gen_all thm =
   let
     val {sign, prop, maxidx, ...} = Thm.rep_thm thm;
     fun elim (th, (x, T)) = Thm.forall_elim (Thm.cterm_of sign (Var ((x, maxidx + 1), T))) th;
diff -r beedc794bd67 -r 7ede865e1fe5 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Fri Jan 11 18:49:25 2002 +0100
+++ b/src/Pure/tactic.ML	Sat Jan 12 16:37:58 2002 +0100
@@ -524,7 +524,7 @@
 
 fun norm_hhf th =
   (if Logic.is_norm_hhf (#prop (Thm.rep_thm th)) then th else rewrite_rule [Drule.norm_hhf_eq] th)
-  |> Drule.forall_elim_vars_safe;
+  |> Drule.gen_all;
 
 val norm_hhf_tac = SUBGOAL (fn (t, i) =>
   if Logic.is_norm_hhf t then all_tac
diff -r beedc794bd67 -r 7ede865e1fe5 src/Sequents/simpdata.ML
--- a/src/Sequents/simpdata.ML	Fri Jan 11 18:49:25 2002 +0100
+++ b/src/Sequents/simpdata.ML	Sat Jan 12 16:37:58 2002 +0100
@@ -240,7 +240,7 @@
   empty_ss setsubgoaler asm_simp_tac
     setSSolver (mk_solver "safe" safe_solver)
     setSolver (mk_solver "unsafe" unsafe_solver)
-    setmksimps (map mk_meta_eq o atomize o forall_elim_vars_safe)
+    setmksimps (map mk_meta_eq o atomize o gen_all)
     setmkcong mk_meta_cong;
 
 val LK_simps =
diff -r beedc794bd67 -r 7ede865e1fe5 src/ZF/Main.ML
--- a/src/ZF/Main.ML	Fri Jan 11 18:49:25 2002 +0100
+++ b/src/ZF/Main.ML	Sat Jan 12 16:37:58 2002 +0100
@@ -4,4 +4,4 @@
   val thy = the_context ();
 end;
 
-simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o forall_elim_vars_safe);
+simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
diff -r beedc794bd67 -r 7ede865e1fe5 src/ZF/OrdQuant.ML
--- a/src/ZF/OrdQuant.ML	Fri Jan 11 18:49:25 2002 +0100
+++ b/src/ZF/OrdQuant.ML	Sat Jan 12 16:37:58 2002 +0100
@@ -103,7 +103,7 @@
 
 val Ord_atomize = atomize (("OrdQuant.oall", [ospec])::ZF_conn_pairs, ZF_mem_pairs);
 
-simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o forall_elim_vars_safe)
+simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all)
                         addsimps [oall_simp, ltD RS beta]
                         addcongs [oall_cong, oex_cong, OUN_cong];
 
diff -r beedc794bd67 -r 7ede865e1fe5 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Fri Jan 11 18:49:25 2002 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Sat Jan 12 16:37:58 2002 +0100
@@ -341,7 +341,7 @@
      (*We use a MINIMAL simpset. Even FOL_ss contains too many simpules.
        If the premises get simplified, then the proofs could fail.*)
      val min_ss = empty_ss
-           setmksimps (map mk_eq o ZF_atomize o forall_elim_vars_safe)
+           setmksimps (map mk_eq o ZF_atomize o gen_all)
            setSolver (mk_solver "minimal"
                       (fn prems => resolve_tac (triv_rls@prems)
                                    ORELSE' assume_tac
diff -r beedc794bd67 -r 7ede865e1fe5 src/ZF/simpdata.ML
--- a/src/ZF/simpdata.ML	Fri Jan 11 18:49:25 2002 +0100
+++ b/src/ZF/simpdata.ML	Sat Jan 12 16:37:58 2002 +0100
@@ -46,7 +46,7 @@
 val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
 
 simpset_ref() :=
-  simpset() setmksimps (map mk_eq o ZF_atomize o forall_elim_vars_safe)
+  simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
   addcongs [if_weak_cong]
   addsplits [split_if]
   setSolver (mk_solver "types" (fn prems => TCSET' (fn tcset => type_solver_tac tcset prems)));