diff -r 9fb068497df4 -r 31b1e4f9af30 doc-src/Logics/FOL.tex
--- a/doc-src/Logics/FOL.tex	Fri Nov 11 10:50:49 1994 +0100
+++ b/doc-src/Logics/FOL.tex	Fri Nov 11 10:53:41 1994 +0100
@@ -339,7 +339,6 @@
 \begin{ttbox} 
 prop_cs    : claset
 FOL_cs     : claset
-FOL_dup_cs : claset
 \end{ttbox}
 \begin{ttdescription}
 \item[\ttindexbold{prop_cs}] contains the propositional rules, namely
@@ -351,13 +350,6 @@
 and the unsafe rules {\tt allE} and~{\tt exI}, as well as rules for
 unique existence.  Search using this is incomplete since quantified
 formulae are used at most once.
-
-\item[\ttindexbold{FOL_dup_cs}] 
-extends {\tt prop_cs} with the safe rules {\tt allI} and~{\tt exE}
-and the unsafe rules {\tt all_dupE} and~{\tt exCI}, as well as
-rules for unique existence.  Search using this is complete --- quantified
-formulae may be duplicated --- but frequently fails to terminate.  It is
-generally unsuitable for depth-first search.
 \end{ttdescription}
 \noindent
 See the file {\tt FOL/FOL.ML} for derivations of the