changeset 37186 | 349e9223c685 |
parent 37136 | e0c9d3e49e15 |
child 37469 | 1436d6f28f17 |
--- a/src/HOL/Tools/record.ML Sat May 29 17:26:02 2010 +0200 +++ b/src/HOL/Tools/record.ML Sat May 29 19:46:29 2010 +0200 @@ -1038,7 +1038,7 @@ 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_global thy) (Future.fork_pri ~1 prf) prop + Goal.future_result (ProofContext.init_global thy) (Goal.fork prf) prop else prf () in Drule.export_without_context thm end;