--- a/doc-src/Ref/simplifier.tex Fri Jan 11 00:35:03 2002 +0100
+++ b/doc-src/Ref/simplifier.tex Fri Jan 11 14:44:24 2002 +0100
@@ -1336,8 +1336,7 @@
object-level, then reflecting them to the meta-level.
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.
+quantifiers from the front of the given theorem.
The function \texttt{atomize} analyses a theorem in order to extract
atomic rewrite rules. The head of all the patterns, matched by the