| changeset 32061 | 11f8ee55662d |
| parent 32058 | c76fd93b3b99 |
| child 32062 | 457f5bcd3d76 |
--- a/src/Pure/Isar/proof.ML Sun Jul 19 19:20:17 2009 +0200 +++ b/src/Pure/Isar/proof.ML Sun Jul 19 19:24:04 2009 +0200 @@ -1043,7 +1043,7 @@ local fun future_terminal_proof proof1 proof2 meths int state = - if int orelse is_relevant state orelse not (Goal.future_enabled ()) + if int orelse is_relevant state orelse not (Goal.local_future_enabled ()) then proof1 meths state else snd (proof2 (fn state' => Future.fork_local ~1 (fn () => ((), proof1 meths state'))) state);