# HG changeset patch
# User wenzelm
# Date 1231356443 -3600
# Node ID d5849935560c97500c6eccc12518be7ef04e4f0a
# Parent  c96b91bab2e60bf11e44b71e6441c3f108b0beb1
Proof.global_future_proof;

diff -r c96b91bab2e6 -r d5849935560c src/Pure/Isar/toplevel.ML
--- 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, _)) =