src/HOL/Tools/record.ML
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;