# HG changeset patch
# User wenzelm
# Date 1010756664 -3600
# Node ID 2d6b5e22e05dc35defeb442c3d67e4cce2d84b87
# Parent  fa4ea2856a31140f082195b6071f1b4962583cc0
tuned;

diff -r fa4ea2856a31 -r 2d6b5e22e05d doc-src/Ref/simplifier.tex
--- 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