tuned;

--- a/NEWS	Tue Mar 25 20:12:53 2014 +0100
+++ b/NEWS	Wed Mar 26 08:59:53 2014 +0100
@@ -550,8 +550,8 @@
 
 * Configuration option "ML_print_depth" controls the pretty-printing
 depth of the ML compiler within the context.  The old print_depth in
-ML is still available as put_default_print_depth, but rarely used.
-Minor INCOMPATIBILITY.
+ML is still available as default_print_depth, but rarely used.  Minor
+INCOMPATIBILITY.
 
 * Proper context discipline for read_instantiate and instantiate_tac:
 variables that are meant to become schematic need to be given as

--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Tue Mar 25 20:12:53 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Wed Mar 26 08:59:53 2014 +0100
@@ -43,7 +43,7 @@
   if test_all @{context} then ()
   else
     (Options.default_put_bool @{option ML_exception_trace} true;
-     put_default_print_depth 200;  (* FIXME proper ML_print_depth within context!? *)
+     default_print_depth 200;  (* FIXME proper ML_print_depth within context!? *)
      PolyML.Compiler.maxInlineSize := 0)
 *}
 

--- a/src/Pure/ML-Systems/polyml.ML	Tue Mar 25 20:12:53 2014 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Wed Mar 26 08:59:53 2014 +0100
@@ -130,8 +130,8 @@
   val depth = Unsynchronized.ref 10;
 in
   fun get_default_print_depth () = ! depth;
-  fun put_default_print_depth n = (depth := n; PolyML.print_depth n);
-  val _ = put_default_print_depth 10;
+  fun default_print_depth n = (depth := n; PolyML.print_depth n);
+  val _ = default_print_depth 10;
 end;
 
 val error_depth = PolyML.error_depth;

--- a/src/Pure/ML-Systems/smlnj.ML	Tue Mar 25 20:12:53 2014 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Wed Mar 26 08:59:53 2014 +0100
@@ -57,11 +57,11 @@
   val depth = ref (10: int);
 in
   fun get_default_print_depth () = ! depth;
-  fun put_default_print_depth n =
+  fun default_print_depth n =
    (depth := n;
     Control.Print.printDepth := dest_int n div 2;
     Control.Print.printLength := dest_int n);
-  val _ = put_default_print_depth 10;
+  val _ = default_print_depth 10;
 end;
 
 val ml_make_string = "(fn _ => \"?\")";

--- a/src/Pure/Tools/proof_general_pure.ML	Tue Mar 25 20:12:53 2014 +0100
+++ b/src/Pure/Tools/proof_general_pure.ML	Wed Mar 26 08:59:53 2014 +0100
@@ -77,7 +77,7 @@
   ProofGeneral.preference ProofGeneral.category_advanced_display
     NONE
     (Markup.print_int o get_default_print_depth)
-    (put_default_print_depth o Markup.parse_int)
+    (default_print_depth o Markup.parse_int)
     ProofGeneral.pgipint
     "print-depth"
     "Setting for the ML print depth";