SimpleThread.fork: uniform handling of outermost Interrupt, which is not an error and should not produce exception trace;

--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Tue Oct 27 10:54:25 2009 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Tue Oct 27 11:25:56 2009 +0100
@@ -271,7 +271,7 @@
                     Markup.markup Markup.sendback "apply metis")
                 | ERROR msg => (false, "Error: " ^ msg);
             val _ = unregister result (Thread.self ());
-          in () end handle Exn.Interrupt => ())
+          in () end)
       in () end);
 
 

--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue Oct 27 10:54:25 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue Oct 27 11:25:56 2009 +0100
@@ -432,7 +432,7 @@
     if auto orelse blocking then
       go ()
     else
-      (SimpleThread.fork true (fn () => (go (); ()) handle Exn.Interrupt => ());
+      (SimpleThread.fork true (fn () => (go (); ()));
        state)
   end
 

--- a/src/Pure/Concurrent/simple_thread.ML	Tue Oct 27 10:54:25 2009 +0100
+++ b/src/Pure/Concurrent/simple_thread.ML	Tue Oct 27 11:25:56 2009 +0100
@@ -15,7 +15,7 @@
 struct
 
 fun fork interrupts body =
-  Thread.fork (fn () => exception_trace (fn () => body ()),
+  Thread.fork (fn () => exception_trace (fn () => body () handle Exn.Interrupt => ()),
     if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts);
 
 fun interrupt thread = Thread.interrupt thread handle Thread _ => ();