make double-sure that the future scheduler is properly shutdown, otherwise its threads are made persistent and will deadlock with the fresh instance after reloading the image (NB: Present.finish involves another Par_List.map over document_variants and thus might fork again);
--- a/src/Pure/System/session.ML Fri Dec 07 23:11:01 2012 +0100
+++ b/src/Pure/System/session.ML Fri Dec 07 23:14:39 2012 +0100
@@ -79,6 +79,7 @@
Keyword.status ();
Outer_Syntax.check_syntax ();
Options.reset_default ();
+ Future.shutdown ();
session_finished := true);