# HG changeset patch
# User oheimb
# Date 982691226 -3600
# Node ID 9e2ec5f02217c36d78a6f7e486d0af7f6a1d2aa8
# Parent  166f7d87b37f62910517215b5b5a215a5004b82a
debugging: replaced gen_all by forall_elim_vars_safe

diff -r 166f7d87b37f -r 9e2ec5f02217 doc-src/Ref/simplifier.tex
--- a/doc-src/Ref/simplifier.tex	Tue Feb 20 13:23:58 2001 +0100
+++ b/doc-src/Ref/simplifier.tex	Tue Feb 20 18:47:06 2001 +0100
@@ -1335,12 +1335,9 @@
 automatically.  Preprocessing involves extracting atomic rewrites at the
 object-level, then reflecting them to the meta-level.
 
-To start, the function \texttt{gen_all} strips any meta-level
-quantifiers from the front of the given theorem.  Usually there are none
+To start, the function \texttt{forall_elim_vars_safe} strips any meta-level
+quantifiers from the front of the given theorem. Usually there are none
 anyway.
-\begin{ttbox}
-fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
-\end{ttbox}
 
 The function \texttt{atomize} analyses a theorem in order to extract
 atomic rewrite rules.  The head of all the patterns, matched by the
@@ -1401,7 +1398,8 @@
   | _ $ (Const("Not",_)$_)      => th RS iff_reflection_F
   | _                           => th RS iff_reflection_T;
 \end{ttbox}
-The three functions \texttt{gen_all}, \texttt{atomize} and \texttt{mk_eq} 
+The 
+three functions \texttt{forall_elim_vars_safe}, \texttt{atomize} and \texttt{mk_eq} 
 will be composed together and supplied below to \texttt{setmksimps}.
 
 
@@ -1429,7 +1427,8 @@
 \end{ttbox}
 %
 The basic simpset for intuitionistic FOL is \ttindexbold{FOL_basic_ss}.  It
-preprocess rewrites using {\tt gen_all}, \texttt{atomize} and \texttt{mk_eq}.
+preprocess rewrites using 
+{\tt forall_elim_vars_safe}, \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.
@@ -1453,7 +1452,7 @@
                addsimprocs [defALL_regroup, defEX_regroup]
                setSSolver   safe_solver
                setSolver  unsafe_solver
-               setmksimps (map mk_eq o atomize o gen_all)
+               setmksimps (map mk_eq o atomize o forall_elim_vars_safe)
                setmkcong mk_meta_cong;
 
 val IFOL_ss = 
diff -r 166f7d87b37f -r 9e2ec5f02217 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Tue Feb 20 13:23:58 2001 +0100
+++ b/src/HOL/simpdata.ML	Tue Feb 20 18:47:06 2001 +0100
@@ -330,8 +330,6 @@
   rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the
   grounds that it allows simplification of R in the two cases.*)
 
-fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
-
 val mksimps_pairs =
   [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
    ("All", [spec]), ("True", []), ("False", []),
@@ -354,7 +352,7 @@
          | _ => [th])
   in atoms end;
 
-fun mksimps pairs = (map mk_eq o mk_atomize pairs o gen_all);
+fun mksimps pairs = (map mk_eq o mk_atomize pairs o forall_elim_vars_safe);
 
 fun unsafe_solver_tac prems =
   FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems), atac, etac FalseE];