clarified print depth;

--- a/src/HOL/Metis.thy	Fri Mar 18 20:35:01 2016 +0100
+++ b/src/HOL/Metis.thy	Fri Mar 18 21:21:09 2016 +0100
@@ -12,7 +12,7 @@
 
 declare [[ML_print_depth = 0]]
 ML_file "~~/src/Tools/Metis/metis.ML"
-declare [[ML_print_depth = 10]]
+declare [[ML_print_depth = 20]]
 
 
 subsection \<open>Literal selection and lambda-lifting helpers\<close>

--- a/src/Pure/General/pretty.ML	Fri Mar 18 20:35:01 2016 +0100
+++ b/src/Pure/General/pretty.ML	Fri Mar 18 21:21:09 2016 +0100
@@ -394,9 +394,7 @@
 
 end;
 
-val _ =
-  PolyML.addPrettyPrinter (fn depth => fn _ => ML_Pretty.to_polyml o to_ML (depth * 2 + 1) o quote);
-
+val _ = PolyML.addPrettyPrinter (fn d => fn _ => ML_Pretty.to_polyml o to_ML (d + 1) o quote);
 val _ = PolyML.addPrettyPrinter (fn _ => fn _ => to_polyml o position);
 
 end;

--- a/src/Pure/ML/ml_pretty.ML	Fri Mar 18 20:35:01 2016 +0100
+++ b/src/Pure/ML/ml_pretty.ML	Fri Mar 18 21:21:09 2016 +0100
@@ -96,7 +96,7 @@
 in
   fun get_print_depth () = ! depth;
   fun print_depth n = (depth := n; PolyML.print_depth n);
-  val _ = print_depth 10;
+  val _ = print_depth 20;
 end;
 
 

--- a/src/Pure/Tools/ml_process.scala	Fri Mar 18 20:35:01 2016 +0100
+++ b/src/Pure/Tools/ml_process.scala	Fri Mar 18 21:21:09 2016 +0100
@@ -68,13 +68,13 @@
 
     val eval_process =
       if (heaps.isEmpty)
-        List("PolyML.print_depth 10")
+        List("PolyML.print_depth 20")
       else
         channel match {
           case None =>
-            List("(ML_Pretty.print_depth 10; Isabelle_Process.init_options ())")
+            List("(ML_Pretty.print_depth 20; Isabelle_Process.init_options ())")
           case Some(ch) =>
-            List("(ML_Pretty.print_depth 10; Isabelle_Process.init_protocol " +
+            List("(ML_Pretty.print_depth 20; Isabelle_Process.init_protocol " +
               ML_Syntax.print_string0(ch.server_name) + ")")
         }