# HG changeset patch
# User wenzelm
# Date 880123256 -3600
# Node ID 349754bdd5b742613c7b755affa84a9addc46ec3
# Parent  2048e7a79d09d215e512fb5fb6caa00e02d57994
SYNC;

diff -r 2048e7a79d09 -r 349754bdd5b7 doc-src/Ref/ref.ind
--- a/doc-src/Ref/ref.ind	Fri Nov 21 15:37:02 1997 +0100
+++ b/doc-src/Ref/ref.ind	Fri Nov 21 15:40:56 1997 +0100
@@ -437,7 +437,7 @@
   \item {\tt prems_of}, \bold{39}
   \item {\tt prems_of_ss}, 105
   \item pretty printing, 70, 72--73, 89
-  \item {\tt Pretty.setdepth}, \bold{3}
+  \item {\tt Pretty.setdepth}, \bold{4}
   \item {\tt Pretty.setmargin}, \bold{4}
   \item {\tt PRIMITIVE}, \bold{25}
   \item {\tt primrec}, 100
@@ -570,7 +570,7 @@
   \item search, 28
     \subitem tacticals, 30--32
   \item {\tt SELECT_GOAL}, 20, \bold{33}
-  \item {\tt Sequence.seq} ML type, 25
+  \item {\tt Seq.seq} ML type, 25
   \item sequences (lazy lists), \bold{26}
   \item sequent calculus, 119
   \item sessions, 1--5