more explicit Simple_Thread.interrupt_unsynchronized, to emphasize its meaning;

--- a/src/HOL/Tools/Sledgehammer/async_manager.ML	Wed Aug 10 14:28:55 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/async_manager.ML	Wed Aug 10 15:17:24 2011 +0200
@@ -144,7 +144,7 @@
               NONE
             else
               let
-                val _ = List.app (Simple_Thread.interrupt o #1) canceling
+                val _ = List.app (Simple_Thread.interrupt_unsynchronized o #1) canceling
                 val canceling' = filter (Thread.isActive o #1) canceling
                 val state' = make_state manager timeout_heap' active canceling' messages store;
               in SOME (map #2 timeout_threads, state') end

--- a/src/Pure/Concurrent/bash.ML	Wed Aug 10 14:28:55 2011 +0200
+++ b/src/Pure/Concurrent/bash.ML	Wed Aug 10 15:17:24 2011 +0200
@@ -73,7 +73,7 @@
       in () end;
 
     fun cleanup () =
-     (Simple_Thread.interrupt system_thread;
+     (Simple_Thread.interrupt_unsynchronized system_thread;
       try File.rm script_path;
       try File.rm output_path;
       try File.rm pid_path);

--- a/src/Pure/Concurrent/simple_thread.ML	Wed Aug 10 14:28:55 2011 +0200
+++ b/src/Pure/Concurrent/simple_thread.ML	Wed Aug 10 15:17:24 2011 +0200
@@ -8,7 +8,7 @@
 sig
   val attributes: bool -> Thread.threadAttribute list
   val fork: bool -> (unit -> unit) -> Thread.thread
-  val interrupt: Thread.thread -> unit
+  val interrupt_unsynchronized: Thread.thread -> unit
   val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
 end;
 
@@ -24,7 +24,7 @@
       body () handle exn => if Exn.is_interrupt exn then () else reraise exn),
     attributes interrupts);
 
-fun interrupt thread = Thread.interrupt thread handle Thread _ => ();
+fun interrupt_unsynchronized thread = Thread.interrupt thread handle Thread _ => ();
 
 
 (* basic synchronization *)

--- a/src/Pure/Concurrent/task_queue.ML	Wed Aug 10 14:28:55 2011 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Wed Aug 10 15:17:24 2011 +0200
@@ -247,7 +247,7 @@
     val running =
       Tasks.fold (#1 #> get_job jobs #> (fn Running t => insert Thread.equal t | _ => I))
         (get_tasks groups (group_id group)) [];
-    val _ = List.app Simple_Thread.interrupt running;
+    val _ = List.app Simple_Thread.interrupt_unsynchronized running;
   in null running end;
 
 fun cancel_all (Queue {jobs, ...}) =
@@ -262,7 +262,7 @@
         | _ => (groups, running))
       end;
     val (running_groups, running) = Task_Graph.fold cancel_job jobs ([], []);
-    val _ = List.app Simple_Thread.interrupt running;
+    val _ = List.app Simple_Thread.interrupt_unsynchronized running;
   in running_groups end;
 
 

--- a/src/Pure/Concurrent/time_limit.ML	Wed Aug 10 14:28:55 2011 +0200
+++ b/src/Pure/Concurrent/time_limit.ML	Wed Aug 10 15:17:24 2011 +0200
@@ -30,12 +30,12 @@
       val main = Thread.self ();
       val timeout = Unsynchronized.ref false;
       val watchdog = Simple_Thread.fork true (fn () =>
-        (OS.Process.sleep time; timeout := true; Thread.interrupt main));
+        (OS.Process.sleep time; timeout := true; Simple_Thread.interrupt_unsynchronized main));
 
       val result =
         Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) ();
 
-      val _ = Thread.interrupt watchdog handle Thread _ => ();
+      val _ = Simple_Thread.interrupt_unsynchronized watchdog;
       val _ = while Thread.isActive watchdog do OS.Process.sleep wait_time;
 
       val test = Exn.capture Multithreading.interrupted ();