src/Pure/proofterm.ML
changeset 41698 90597e044e5f
parent 41674 7da257539a8d
child 41699 21492e1c2b5a
     1.1 --- a/src/Pure/proofterm.ML	Thu Feb 03 18:57:42 2011 +0100
     1.2 +++ b/src/Pure/proofterm.ML	Thu Feb 03 19:21:12 2011 +0100
     1.3 @@ -52,6 +52,7 @@
     1.4    val approximate_proof_body: proof -> proof_body
     1.5  
     1.6    (** primitive operations **)
     1.7 +  val proofs_enabled: unit -> bool
     1.8    val proof_combt: proof * term list -> proof
     1.9    val proof_combt': proof * term option list -> proof
    1.10    val proof_combP: proof * proof list -> proof
    1.11 @@ -973,6 +974,7 @@
    1.12  (***** axioms and theorems *****)
    1.13  
    1.14  val proofs = Unsynchronized.ref 2;
    1.15 +fun proofs_enabled () = ! proofs >= 2;
    1.16  
    1.17  fun vars_of t = map Var (rev (Term.add_vars t []));
    1.18  fun frees_of t = map Free (rev (Term.add_frees t []));
    1.19 @@ -1444,7 +1446,7 @@
    1.20  
    1.21      fun make_body0 proof0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
    1.22      val body0 =
    1.23 -      if ! proofs <> 2 then Future.value (make_body0 MinProof)
    1.24 +      if not (proofs_enabled ()) then Future.value (make_body0 MinProof)
    1.25        else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ()))
    1.26        else
    1.27          singleton
    1.28 @@ -1453,6 +1455,7 @@
    1.29  
    1.30      fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
    1.31      val (i, body') =
    1.32 +      (* FIXME non-deterministic!? depends on fulfilled proof*)
    1.33        (case strip_combt (fst (strip_combP prf)) of
    1.34          (PThm (i, ((old_name, prop', NONE), body')), args') =>
    1.35            if (old_name = "" orelse old_name = name) andalso prop1 = prop' andalso args = args'