src/Pure/goal.ML

             if Unify.matches_list thy [Thm.term_of stmt] [Thm.prop_of res]
             then Thm.check_shyps sorts res
             else err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res))
           end);
     val res =
-      if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 then result ()
+      if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (Future.enabled ())
+      then result ()
       else future_result ctxt' (Future.fork_background result) (Thm.term_of stmt);
   in
     Conjunction.elim_balanced (length props) res
     |> map (Assumption.export false ctxt' ctxt)
     |> Variable.export ctxt' ctxt