
diff -r d66477d29598 -r 7cfc85fc6fd7 doc-src/Ref/simplifier.tex
--- a/doc-src/Ref/simplifier.tex	Sat Apr 04 14:27:11 1998 +0200
+++ b/doc-src/Ref/simplifier.tex	Sat Apr 04 14:30:19 1998 +0200
@@ -1308,14 +1308,11 @@
 
 \subsection{Making the initial simpset}
 
-It is time to assemble these items.  We open module \texttt{Simplifier}
-to gain direct access to its components.  We define the infix operator
+It is time to assemble these items.  We define the infix operator
 \ttindex{addcongs} to insert congruence rules; given a list of
 theorems, it converts their conclusions into meta-equalities and
 passes them to \ttindex{addeqcongs}.
 \begin{ttbox}
-open Simplifier;
-\ttbreak
 infix 4 addcongs;
 fun ss addcongs congs =
     ss addeqcongs (congs RL [eq_reflection,iff_reflection]);




