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