# HG changeset patch
# User wenzelm
# Date 1300910257 -3600
# Node ID d5bf0ce40bd7374fd88e9649c205a5d3ccff71c5
# Parent  96c50a4210a2e40d9e40ce9234909df734d7f3bc
isolate change of Proofterm.proofs in TPTP.thy from rest of session;
qualified Proofterm.proofs to facilitate grepping;

diff -r 96c50a4210a2 -r d5bf0ce40bd7 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Wed Mar 23 20:51:36 2011 +0100
+++ b/src/HOL/ex/ROOT.ML	Wed Mar 23 20:57:37 2011 +0100
@@ -73,10 +73,12 @@
   "Quicksort",
   "Birthday_Paradoxon",
   "List_to_Set_Comprehension_Examples",
-  "Set_Algebras",
-  "TPTP"
+  "Set_Algebras"
 ];
 
+Unsynchronized.setmp Proofterm.proofs (! Proofterm.proofs)
+  use_thy "TPTP";
+
 if getenv "ISABELLE_GHC" = "" then ()
 else use_thy "Quickcheck_Narrowing_Examples";
 
diff -r 96c50a4210a2 -r d5bf0ce40bd7 src/HOL/ex/TPTP.thy
--- a/src/HOL/ex/TPTP.thy	Wed Mar 23 20:51:36 2011 +0100
+++ b/src/HOL/ex/TPTP.thy	Wed Mar 23 20:57:37 2011 +0100
@@ -14,7 +14,7 @@
 
 declare [[smt_oracle]]
 
-ML {* proofs := 0 *}
+ML {* Proofterm.proofs := 0 *}
 
 ML {*
 fun SOLVE_TIMEOUT seconds name tac st =