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 =