diff -r b0ebac91c8d5 -r c2432d193705 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Thu Sep 25 20:34:17 2008 +0200
+++ b/src/Pure/goal.ML	Thu Sep 25 20:34:18 2008 +0200
@@ -122,7 +122,7 @@
       Drule.implies_intr_list assms o
       Thm.adjust_maxidx_thm ~1 o result;
     val local_result =
-      Thm.promise (Future.fork_irrelevant global_result) (cert global_prop)
+      Thm.promise global_result (cert global_prop)
       |> Thm.instantiate (instT, [])
       |> Drule.forall_elim_list fixes
       |> fold (Thm.elim_implies o Thm.assume) assms;
@@ -176,7 +176,7 @@
           end);
     val res =
       if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 then result ()
-      else promise_result ctxt result (Thm.term_of stmt);
+      else promise_result ctxt' result (Thm.term_of stmt);
   in
     Conjunction.elim_balanced (length props) res
     |> map (Assumption.export false ctxt' ctxt)