reraise interrupt exceptions

--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Dec 06 09:54:58 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Dec 06 10:23:31 2010 +0100
@@ -616,8 +616,12 @@
           else
             (really_go ()
              handle ERROR message => ("unknown", "Error: " ^ message ^ "\n")
-                  | exn => ("unknown", "Internal error:\n" ^
-                                       ML_Compiler.exn_message exn ^ "\n"))
+                  | exn =>
+                    if Exn.is_interrupt exn then
+                      reraise exn
+                    else
+                      ("unknown", "Internal error:\n" ^
+                                  ML_Compiler.exn_message exn ^ "\n"))
         val _ =
           if expect = "" orelse outcome_code = expect then
             ()