src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy

--- 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)
 *}