# HG changeset patch
# User wenzelm
# Date 1296757272 -3600
# Node ID 90597e044e5f68c717f4fb503305364551007155
# Parent  19890332febc3e66a2afa43da449b98763871d2f
clarified Proofterm.proofs_enabled;

diff -r 19890332febc -r 90597e044e5f src/HOL/Tools/Datatype/datatype_realizer.ML
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Thu Feb 03 18:57:42 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Thu Feb 03 19:21:12 2011 +0100
@@ -214,7 +214,7 @@
   end;
 
 fun add_dt_realizers config names thy =
-  if ! Proofterm.proofs < 2 then thy
+  if not (Proofterm.proofs_enabled ()) then thy
   else
     let
       val _ = Datatype_Aux.message config "Adding realizers for induction and case analysis ...";
diff -r 19890332febc -r 90597e044e5f src/Pure/ProofGeneral/preferences.ML
--- a/src/Pure/ProofGeneral/preferences.ML	Thu Feb 03 18:57:42 2011 +0100
+++ b/src/Pure/ProofGeneral/preferences.ML	Thu Feb 03 19:21:12 2011 +0100
@@ -84,7 +84,7 @@
 
 val proof_pref = Unsynchronized.setmp Proofterm.proofs 1 (fn () =>
   let
-    fun get () = PgipTypes.bool_to_pgstring (! Proofterm.proofs >= 2);
+    fun get () = PgipTypes.bool_to_pgstring (Proofterm.proofs_enabled ());
     fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1);
   in mkpref get set PgipTypes.Pgipbool "full-proofs" "Record full proof objects internally" end) ();
 
diff -r 19890332febc -r 90597e044e5f src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Feb 03 18:57:42 2011 +0100
+++ b/src/Pure/proofterm.ML	Thu Feb 03 19:21:12 2011 +0100
@@ -52,6 +52,7 @@
   val approximate_proof_body: proof -> proof_body
 
   (** primitive operations **)
+  val proofs_enabled: unit -> bool
   val proof_combt: proof * term list -> proof
   val proof_combt': proof * term option list -> proof
   val proof_combP: proof * proof list -> proof
@@ -973,6 +974,7 @@
 (***** axioms and theorems *****)
 
 val proofs = Unsynchronized.ref 2;
+fun proofs_enabled () = ! proofs >= 2;
 
 fun vars_of t = map Var (rev (Term.add_vars t []));
 fun frees_of t = map Free (rev (Term.add_frees t []));
@@ -1444,7 +1446,7 @@
 
     fun make_body0 proof0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
     val body0 =
-      if ! proofs <> 2 then Future.value (make_body0 MinProof)
+      if not (proofs_enabled ()) then Future.value (make_body0 MinProof)
       else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ()))
       else
         singleton
@@ -1453,6 +1455,7 @@
 
     fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
     val (i, body') =
+      (* FIXME non-deterministic!? depends on fulfilled proof*)
       (case strip_combt (fst (strip_combP prf)) of
         (PThm (i, ((old_name, prop', NONE), body')), args') =>
           if (old_name = "" orelse old_name = name) andalso prop1 = prop' andalso args = args'