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