Toplevel.thread provides Isar-style exception output;

--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Tue Nov 10 23:15:20 2009 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Tue Nov 10 23:18:03 2009 +0100
@@ -119,7 +119,7 @@
 fun check_thread_manager () = Synchronized.change global_state
   (fn state as {manager, timeout_heap, active, cancelling, messages, store} =>
     if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
-    else let val manager = SOME (SimpleThread.fork false (fn () =>
+    else let val manager = SOME (Toplevel.thread false (fn () =>
       let
         fun time_limit timeout_heap =
           (case try Thread_Heap.min timeout_heap of
@@ -258,7 +258,7 @@
           "external prover " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
             Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
 
-        val _ = SimpleThread.fork true (fn () =>
+        val _ = Toplevel.thread true (fn () =>
           let
             val _ = register birth_time death_time (Thread.self (), desc);
             val problem = ATP_Wrapper.problem_of_goal (! full_types) i (ctxt, (facts, goal));

--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue Nov 10 23:15:20 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue Nov 10 23:18:03 2009 +0100
@@ -427,7 +427,7 @@
                            |>> equal "genuine")
   in
     if auto orelse blocking then go ()
-    else (SimpleThread.fork true (fn () => (go (); ())); (false, state))
+    else (Toplevel.thread true (fn () => (go (); ())); (false, state))
   end
 
 (* (TableFun().key * string list) list option * int option

--- a/src/Pure/Isar/toplevel.ML	Tue Nov 10 23:15:20 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Nov 10 23:18:03 2009 +0100
@@ -33,6 +33,7 @@
   exception TERMINATE
   exception TOPLEVEL_ERROR
   val program: (unit -> 'a) -> 'a
+  val thread: bool -> (unit -> unit) -> Thread.thread
   type transition
   val empty: transition
   val init_of: transition -> string option
@@ -226,10 +227,18 @@
 exception EXCURSION_FAIL = Runtime.EXCURSION_FAIL;
 exception TOPLEVEL_ERROR = Runtime.TOPLEVEL_ERROR;
 
-fun program f =
- (f
+fun program body =
+ (body
   |> Runtime.controlled_execution
-  |> Runtime.toplevel_error ML_Compiler.exn_message) ();
+  |> Runtime.toplevel_error (Output.error_msg o ML_Compiler.exn_message)) ();
+
+fun thread interrupts body =
+  Thread.fork
+    (((fn () => body () handle Exn.Interrupt => ())
+        |> Runtime.debugging
+        |> Runtime.toplevel_error
+          (fn exn => priority ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))),
+      SimpleThread.attributes interrupts);
 
 
 (* node transactions -- maintaining stable checkpoints *)