discontinued Pretty.setdepth, which appears to be largely unused, but can disrupt important markup if enabled accidentally;

--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sat May 08 19:18:28 2010 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sat May 08 19:53:11 2010 +0200
@@ -212,7 +212,6 @@
 
 text {*
   \begin{mldecls}
-    @{index_ML Pretty.setdepth: "int -> unit"} \\
     @{index_ML Pretty.margin_default: "int Unsynchronized.ref"} \\
     @{index_ML print_depth: "int -> unit"} \\
   \end{mldecls}
@@ -221,12 +220,6 @@
 
   \begin{description}
 
-  \item @{ML Pretty.setdepth}~@{text d} tells the pretty printer to
-  limit the printing depth to @{text d}.  This affects the display of
-  types, terms, theorems etc.  The default value is 0, which permits
-  printing to an arbitrary depth.  Other useful values for @{text d}
-  are 10 and 20.
-
   \item @{ML Pretty.margin_default} indicates the global default for
   the right margin of the built-in pretty printer, with initial value
   76.  Note that user-interfaces typically control margins

--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Sat May 08 19:18:28 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Sat May 08 19:53:11 2010 +0200
@@ -231,7 +231,6 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-    \indexdef{}{ML}{Pretty.setdepth}\verb|Pretty.setdepth: int -> unit| \\
     \indexdef{}{ML}{Pretty.margin\_default}\verb|Pretty.margin_default: int Unsynchronized.ref| \\
     \indexdef{}{ML}{print\_depth}\verb|print_depth: int -> unit| \\
   \end{mldecls}
@@ -240,12 +239,6 @@
 
   \begin{description}
 
-  \item \verb|Pretty.setdepth|~\isa{d} tells the pretty printer to
-  limit the printing depth to \isa{d}.  This affects the display of
-  types, terms, theorems etc.  The default value is 0, which permits
-  printing to an arbitrary depth.  Other useful values for \isa{d}
-  are 10 and 20.
-
   \item \verb|Pretty.margin_default| indicates the global default for
   the right margin of the built-in pretty printer, with initial value
   76.  Note that user-interfaces typically control margins

--- a/src/Pure/General/pretty.ML	Sat May 08 19:18:28 2010 +0200
+++ b/src/Pure/General/pretty.ML	Sat May 08 19:53:11 2010 +0200
@@ -53,7 +53,6 @@
   val indent: int -> T -> T
   val unbreakable: T -> T
   val margin_default: int Unsynchronized.ref
-  val setdepth: int -> unit
   val to_ML: T -> ML_Pretty.pretty
   val from_ML: ML_Pretty.pretty -> T
   val symbolicN: string
@@ -184,22 +183,6 @@
 val margin_default = Unsynchronized.ref 76;  (*right margin, or page width*)
 
 
-(* depth limitation *)
-
-val depth = Unsynchronized.ref 0;   (*maximum depth; 0 means no limit*)
-fun setdepth dp = (depth := dp);
-
-local
-  fun pruning dp (Block (m, bes, indent, _)) =
-        if dp > 0
-        then block_markup m (indent, map (pruning (dp - 1)) bes)
-        else str "..."
-    | pruning _ e = e;
-in
-  fun prune e = if ! depth > 0 then pruning (! depth) e else e;
-end;
-
-
 (* formatted output *)
 
 local
@@ -289,7 +272,7 @@
                   else text |> newline |> indentation block)
           | String str => format (es, block, after) (string str text));
   in
-    #tx (format ([prune input], (Buffer.empty, 0), 0) empty)
+    #tx (format ([input], (Buffer.empty, 0), 0) empty)
   end;
 
 end;
@@ -314,7 +297,7 @@
     fun fmt (Block ((bg, en), prts, _, _)) = Buffer.add bg #> fold fmt prts #> Buffer.add en
       | fmt (String (s, _)) = Buffer.add s
       | fmt (Break (_, wd)) = Buffer.add (output_spaces wd);
-  in fmt (prune prt) Buffer.empty end;
+  in fmt prt Buffer.empty end;
 
 
 (* ML toplevel pretty printing *)