src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy

--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Tue Mar 25 17:59:34 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Tue Mar 25 19:03:02 2014 +0100
@@ -42,8 +42,8 @@
 ML {*
   if test_all @{context} then ()
   else
-    (Options.default_put_bool @{option exception_trace} true;
-     PolyML.print_depth 200;
+    (Options.default_put_bool @{option ML_exception_trace} true;
+     put_default_print_depth 200;  (* FIXME proper ML_print_depth within context!? *)
      PolyML.Compiler.maxInlineSize := 0)
 *}
 
@@ -186,8 +186,9 @@
      prob_names;
 *}
 
+declare [[ML_print_depth = 2000]]
+
 ML {*
-print_depth 2000;
 the_tactics
 |> map (filter (fn (_, _, x) => is_none x)
         #> map (fn (x, SOME y, _) => (x, cterm_of @{theory} y)))