# HG changeset patch
# User wenzelm
# Date 1439466948 -7200
# Node ID 0ccb5fb83c24ef774981d9af2210a266553d69d1
# Parent  90659d0215bd3fdd66f8d470dcfe070804269bd4
more standard options;
refrain from accessing PolyML internals;

diff -r 90659d0215bd -r 0ccb5fb83c24 src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Thu Aug 13 11:40:31 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Thu Aug 13 13:55:48 2015 +0200
@@ -4,7 +4,6 @@
 Various tests for the proof reconstruction module.
 
 NOTE
-  - Makes use of the PolyML structure.
   - looks for THF proofs in the path indicated by $THF_PROOFS
   - these proofs are generated using LEO-II with the following
     configuration choices: -po 1 -nux -nuc --expand_extuni
@@ -39,13 +38,7 @@
   tptp_max_term_size = 0
 ]]
 
-ML {*
-  if test_all @{context} then ()
-  else
-    (Options.default_put_bool @{system_option ML_exception_trace} true;
-     default_print_depth 200;  (* FIXME proper ML_print_depth within context!? *)
-     PolyML.Compiler.maxInlineSize := 0)
-*}
+declare [[ML_exception_trace, ML_print_depth = 200]]
 
 
 section "Importing proofs"
diff -r 90659d0215bd -r 0ccb5fb83c24 src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy	Thu Aug 13 11:40:31 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy	Thu Aug 13 13:55:48 2015 +0200
@@ -2,9 +2,6 @@
     Author:     Nik Sultana, Cambridge University Computer Laboratory
 
 Unit tests for proof reconstruction module.
-
-NOTE
-  - Makes use of the PolyML structure.
 *)
 
 theory TPTP_Proof_Reconstruction_Test_Units
@@ -12,15 +9,8 @@
 begin
 
 declare [[ML_exception_trace, ML_print_depth = 200]]
-ML {*
-PolyML.Compiler.maxInlineSize := 0;
-(* FIXME doesn't work with Isabelle?
-   PolyML.Compiler.debug := true *)
-*}
 
-declare [[
-  tptp_trace_reconstruction = true
-]]
+declare [[tptp_trace_reconstruction = true]]
 
 lemma "! (X1 :: bool) (X2 :: bool) (X3 :: bool) (X4 :: bool) (X5 :: bool). P \<Longrightarrow> ! (X1 :: bool) (X3 :: bool) (X5 :: bool). P"
 apply (tactic {*canonicalise_qtfr_order @{context} 1*})