# HG changeset patch
# User wenzelm
# Date 863701186 -7200
# Node ID 6baf8e01f4e53937b3904cb4ae1a1c47a6675e94
# Parent  7c3cbf675e85f4db6a29ba7cf0a1c47735da5f27
SYNC;

diff -r 7c3cbf675e85 -r 6baf8e01f4e5 doc-src/Ref/ref.ind
--- a/doc-src/Ref/ref.ind	Thu May 15 14:59:25 1997 +0200
+++ b/doc-src/Ref/ref.ind	Thu May 15 14:59:46 1997 +0200
@@ -240,7 +240,7 @@
     \subitem of simplification, 106
     \subitem of translations, 92
   \item exceptions
-    \subitem printing of, 4
+    \subitem printing of, 5
   \item {\tt exit}, \bold{2}
   \item {\tt extensional}, \bold{44}
 
@@ -428,7 +428,7 @@
   \item {\tt prems_of_ss}, 105
   \item pretty printing, 70, 72--73, 89
   \item {\tt Pretty.setdepth}, \bold{3}
-  \item {\tt Pretty.setmargin}, \bold{3}
+  \item {\tt Pretty.setmargin}, \bold{4}
   \item {\tt PRIMITIVE}, \bold{25}
   \item {\tt primrec}, 100
   \item {\tt prin}, 5, \bold{14}