--- a/src/HOL/Tools/record.ML Mon Nov 16 12:09:59 2009 +0100
+++ b/src/HOL/Tools/record.ML Mon Nov 16 13:49:21 2009 +0100
@@ -1009,14 +1009,20 @@
(** record simprocs **)
fun future_forward_prf_standard thy prf prop () =
- let val thm = if !quick_and_dirty then Skip_Proof.make_thm thy prop
- else Goal.future_result (ProofContext.init thy) (Future.fork_pri ~1 prf) prop;
- in Drule.standard thm end;
+ let val thm =
+ if ! quick_and_dirty then Skip_Proof.make_thm thy prop
+ else if Goal.future_enabled () then
+ Goal.future_result (ProofContext.init thy) (Future.fork_pri ~1 prf) prop
+ else prf ()
+ in Drule.standard thm end;
fun prove_common immediate stndrd thy asms prop tac =
- let val prv = if !quick_and_dirty then Skip_Proof.prove
- else if immediate then Goal.prove else Goal.prove_future;
- val prf = prv (ProofContext.init thy) [] asms prop tac
+ let
+ val prv =
+ if ! quick_and_dirty then Skip_Proof.prove
+ else if immediate orelse not (Goal.future_enabled ()) then Goal.prove
+ else Goal.prove_future;
+ val prf = prv (ProofContext.init thy) [] asms prop tac;
in if stndrd then Drule.standard prf else prf end;
val prove_future_global = prove_common false;