# HG changeset patch
# User wenzelm
# Date 1228518208 -3600
# Node ID 3f7ca7fec74c6b5530f14e553be6be74d7e98dae
# Parent  23cbaa9f9834d2d8730f824605b4b306a66d6723
excursion: improve parallelism by not joining proofs here (depends on persistent checkpoints);

diff -r 23cbaa9f9834 -r 3f7ca7fec74c src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sat Dec 06 00:02:11 2008 +0100
+++ b/src/Pure/Isar/toplevel.ML	Sat Dec 06 00:03:28 2008 +0100
@@ -744,7 +744,7 @@
     val (future_results, end_state) = fold_map (proof_result immediate) input toplevel;
     val _ =
       (case end_state of
-        State (NONE, SOME (Theory (Context.Theory thy, _), _)) => PureThy.force_proofs thy
+        State (NONE, SOME (Theory (Context.Theory _, _), _)) => ()
       | _ => error "Unfinished development at end of input");
     val results = maps Lazy.force future_results;
   in (results, fn () => ignore (command (commit_exit end_pos) end_state)) end);