1.1 --- a/src/HOL/ex/ROOT.ML	Wed Mar 23 20:51:36 2011 +0100
     1.2 +++ b/src/HOL/ex/ROOT.ML	Wed Mar 23 20:57:37 2011 +0100
     1.3 @@ -73,10 +73,12 @@
     1.4    "Quicksort",
     1.5    "Birthday_Paradoxon",
     1.6    "List_to_Set_Comprehension_Examples",
     1.7 -  "Set_Algebras",
     1.8 -  "TPTP"
     1.9 +  "Set_Algebras"
    1.10  ];
    1.11  
    1.12 +Unsynchronized.setmp Proofterm.proofs (! Proofterm.proofs)
    1.13 +  use_thy "TPTP";
    1.14 +
    1.15  if getenv "ISABELLE_GHC" = "" then ()
    1.16  else use_thy "Quickcheck_Narrowing_Examples";
    1.17  

     2.1 --- a/src/HOL/ex/TPTP.thy	Wed Mar 23 20:51:36 2011 +0100
     2.2 +++ b/src/HOL/ex/TPTP.thy	Wed Mar 23 20:57:37 2011 +0100
     2.3 @@ -14,7 +14,7 @@
     2.4  
     2.5  declare [[smt_oracle]]
     2.6  
     2.7 -ML {* proofs := 0 *}
     2.8 +ML {* Proofterm.proofs := 0 *}
     2.9  
    2.10  ML {*
    2.11  fun SOLVE_TIMEOUT seconds name tac st =