# HG changeset patch
# User blanchet
# Date 1291627411 -3600
# Node ID 79d2ea0e1fdbd695970e297cf3bd5ed49f27f294
# Parent  9140c5950494dd31e6ec30cf844c6b9ef4692ee2
reraise interrupt exceptions

diff -r 9140c5950494 -r 79d2ea0e1fdb src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- 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
             ()