changeset 32062 | 457f5bcd3d76 |
parent 32061 | 11f8ee55662d |
child 32089 | 568a23753e3a |
--- a/src/Pure/goal.ML Sun Jul 19 19:24:04 2009 +0200 +++ b/src/Pure/goal.ML Mon Jul 20 00:37:39 2009 +0200 @@ -188,7 +188,7 @@ val res = if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (future_enabled ()) then result () - else future_result ctxt' (Future.fork_local ~1 result) (Thm.term_of stmt); + else future_result ctxt' (Future.fork_pri ~1 result) (Thm.term_of stmt); in Conjunction.elim_balanced (length props) res |> map (Assumption.export false ctxt' ctxt)