author | wenzelm |
Wed, 07 Jan 2009 20:27:23 +0100 | |
changeset 29386 | d5849935560c |
parent 29385 | c96b91bab2e6 |
child 29387 | d23fdfa46b6a |
--- a/src/Pure/Isar/toplevel.ML Wed Jan 07 20:27:05 2009 +0100 +++ b/src/Pure/Isar/toplevel.ML Wed Jan 07 20:27:23 2009 +0100 @@ -718,7 +718,7 @@ val (body_trs, end_tr) = split_last proof_trs; val finish = Context.Theory o ProofContext.theory_of; - val future_proof = Proof.future_proof + val future_proof = Proof.global_future_proof (fn prf => Future.fork_pri ~1 (fn () => let val (states, State (result_node, _)) =