# HG changeset patch
# User wenzelm
# Date 1358267326 -3600
# Node ID cb2b940e2fdf429827ccb1f49a6d42ec9190a4be
# Parent  f4a6c360af35c5e28c83fb86d83ae6bf591f68f8
avoid handling arbitrary exceptions, notably physical interrupts that would make the program erratic;

diff -r f4a6c360af35 -r cb2b940e2fdf src/HOL/Matrix_LP/Cplex_tools.ML
--- a/src/HOL/Matrix_LP/Cplex_tools.ML	Tue Jan 15 16:34:19 2013 +0100
+++ b/src/HOL/Matrix_LP/Cplex_tools.ML	Tue Jan 15 17:28:46 2013 +0100
@@ -1148,7 +1148,7 @@
         result
     end
     handle (Load_cplexResult s) => raise (Execute ("Load_cplexResult: "^s^"\nExecute: "^answer))
-         | _ => raise (Execute answer)  (* FIXME avoid handle _ *)
+         | exn => if Exn.is_interrupt exn then reraise exn else raise (Execute answer)
     end
 
 fun solve_cplex prog =
diff -r f4a6c360af35 -r cb2b940e2fdf src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Tue Jan 15 16:34:19 2013 +0100
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Tue Jan 15 17:28:46 2013 +0100
@@ -166,10 +166,10 @@
         case lhs_eq of
           SOME (Const (@{const_name HOL.eq}, _) $ _ $ _) => SOME (@{thm refl} RS thm)
           | SOME _ => (case body_type (fastype_of lhs) of
-            Type (typ_name, _) => ( SOME
-              (#equiv_thm (the (Quotient_Info.lookup_quotients lthy typ_name)) 
-                RS @{thm Equiv_Relations.equivp_reflp} RS thm)
-              handle _ => NONE)
+            Type (typ_name, _) =>
+              try (fn () =>
+                #equiv_thm (the (Quotient_Info.lookup_quotients lthy typ_name)) 
+                  RS @{thm Equiv_Relations.equivp_reflp} RS thm) ()
             | _ => NONE
             )
           | _ => NONE
diff -r f4a6c360af35 -r cb2b940e2fdf src/HOL/Word/WordBitwise.thy
--- a/src/HOL/Word/WordBitwise.thy	Tue Jan 15 16:34:19 2013 +0100
+++ b/src/HOL/Word/WordBitwise.thy	Tue Jan 15 17:28:46 2013 +0100
@@ -514,10 +514,12 @@
       |> mk_nat_clist;
     val prop = Thm.mk_binop @{cterm "op = :: nat list => _"} ct ns
                  |> Thm.apply @{cterm Trueprop};
-  in Goal.prove_internal [] prop 
-      (K (REPEAT_DETERM (resolve_tac @{thms upt_eq_list_intros} 1
-          ORELSE simp_tac word_ss 1))) |> mk_meta_eq |> SOME end
-    handle TERM _ => NONE
+  in
+    try (fn () =>
+      Goal.prove_internal [] prop 
+        (K (REPEAT_DETERM (resolve_tac @{thms upt_eq_list_intros} 1
+            ORELSE simp_tac word_ss 1))) |> mk_meta_eq) ()
+  end
   | _ => NONE;
 
 val expand_upt_simproc = Simplifier.make_simproc