excursion: improve parallelism by not joining proofs here (depends on persistent checkpoints);

--- 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);