src/Pure/goal.ML
changeset 29088 95a239a5e055
parent 28973 c549650d1442
child 29122 b3bae49a013a
     1.1 --- a/src/Pure/goal.ML	Thu Dec 11 22:53:50 2008 +0100
     1.2 +++ b/src/Pure/goal.ML	Fri Dec 12 12:14:02 2008 +0100
     1.3 @@ -177,7 +177,8 @@
     1.4              else err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res))
     1.5            end);
     1.6      val res =
     1.7 -      if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 then result ()
     1.8 +      if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (Future.enabled ())
     1.9 +      then result ()
    1.10        else future_result ctxt' (Future.fork_background result) (Thm.term_of stmt);
    1.11    in
    1.12      Conjunction.elim_balanced (length props) res