guard future proofs by Goal.future_enabled;
authorwenzelm
Mon Nov 16 13:49:21 2009 +0100 (2009-11-16)
changeset 337112fdb11580b96
parent 33710 ffc5176a9105
child 33712 cffc97238102
guard future proofs by Goal.future_enabled;
src/HOL/Tools/record.ML
     1.1 --- a/src/HOL/Tools/record.ML	Mon Nov 16 12:09:59 2009 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Mon Nov 16 13:49:21 2009 +0100
     1.3 @@ -1009,14 +1009,20 @@
     1.4  (** record simprocs **)
     1.5  
     1.6  fun future_forward_prf_standard thy prf prop () =
     1.7 -   let val thm = if !quick_and_dirty then Skip_Proof.make_thm thy prop 
     1.8 -                 else Goal.future_result (ProofContext.init thy) (Future.fork_pri ~1 prf) prop;
     1.9 -   in Drule.standard thm end;
    1.10 +  let val thm =
    1.11 +    if ! quick_and_dirty then Skip_Proof.make_thm thy prop
    1.12 +    else if Goal.future_enabled () then
    1.13 +      Goal.future_result (ProofContext.init thy) (Future.fork_pri ~1 prf) prop
    1.14 +    else prf ()
    1.15 +  in Drule.standard thm end;
    1.16  
    1.17  fun prove_common immediate stndrd thy asms prop tac =
    1.18 -  let val prv = if !quick_and_dirty then Skip_Proof.prove 
    1.19 -                else if immediate then Goal.prove else Goal.prove_future;
    1.20 -      val prf = prv (ProofContext.init thy) [] asms prop tac
    1.21 +  let
    1.22 +    val prv =
    1.23 +      if ! quick_and_dirty then Skip_Proof.prove
    1.24 +      else if immediate orelse not (Goal.future_enabled ()) then Goal.prove
    1.25 +      else Goal.prove_future;
    1.26 +    val prf = prv (ProofContext.init thy) [] asms prop tac;
    1.27    in if stndrd then Drule.standard prf else prf end;
    1.28  
    1.29  val prove_future_global = prove_common false;