diff -r dd7dcb9b2637 -r 2b61c5e27399 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Tue Aug 10 12:09:53 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML	Tue Aug 10 12:29:11 2010 +0200
@@ -105,6 +105,10 @@
     val _ = quick_and_dirty := true;  (* FIXME !? *)
     val _ = Keyword.status ();
     val _ = Output.status (Markup.markup Markup.ready "");
-  in Isar.toplevel_loop in_stream {init = true, welcome = false, sync = true, secure = true} end;
+    val _ =
+      Simple_Thread.fork false (fn () =>
+        (Isar.toplevel_loop in_stream {init = true, welcome = false, sync = true, secure = true};
+          quit ()));
+  in () end;
 
 end;