# HG changeset patch
# User wenzelm
# Date 1284049054 -7200
# Node ID 2ec7afadc3444241890648b09793665faef9be80
# Parent  cda88e68106dd7b184085ecb5884cf65ed65861b
avoid handling interrupts in user code;

diff -r cda88e68106d -r 2ec7afadc344 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Thu Sep 09 18:04:35 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Thu Sep 09 18:17:34 2010 +0200
@@ -1299,10 +1299,13 @@
                     end
                   | NONE => (thy,NONE)
             end
-    end  (* FIXME avoid handle _ *)
+    end
     handle e =>
-      (if_debug (fn () => writeln ("Exception in get_isabelle_thm:\n" ^ ML_Compiler.exn_message e)) ();
-        (thy,NONE))
+      if Exn.is_interrupt e then reraise e
+      else
+        (if_debug (fn () =>
+            writeln ("Exception in get_isabelle_thm:\n" ^ ML_Compiler.exn_message e)) ();
+          (thy,NONE))
 
 fun get_isabelle_thm_and_warn thyname thmname hol4conc thy =
   let