1.1 --- a/src/HOL/Matrix_LP/Cplex_tools.ML	Tue Jan 15 16:34:19 2013 +0100
     1.2 +++ b/src/HOL/Matrix_LP/Cplex_tools.ML	Tue Jan 15 17:28:46 2013 +0100
     1.3 @@ -1148,7 +1148,7 @@
     1.4          result
     1.5      end
     1.6      handle (Load_cplexResult s) => raise (Execute ("Load_cplexResult: "^s^"\nExecute: "^answer))
     1.7 -         | _ => raise (Execute answer)  (* FIXME avoid handle _ *)
     1.8 +         | exn => if Exn.is_interrupt exn then reraise exn else raise (Execute answer)
     1.9      end
    1.10  
    1.11  fun solve_cplex prog =

     2.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Tue Jan 15 16:34:19 2013 +0100
     2.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Tue Jan 15 17:28:46 2013 +0100
     2.3 @@ -166,10 +166,10 @@
     2.4          case lhs_eq of
     2.5            SOME (Const (@{const_name HOL.eq}, _) $ _ $ _) => SOME (@{thm refl} RS thm)
     2.6            | SOME _ => (case body_type (fastype_of lhs) of
     2.7 -            Type (typ_name, _) => ( SOME
     2.8 -              (#equiv_thm (the (Quotient_Info.lookup_quotients lthy typ_name)) 
     2.9 -                RS @{thm Equiv_Relations.equivp_reflp} RS thm)
    2.10 -              handle _ => NONE)
    2.11 +            Type (typ_name, _) =>
    2.12 +              try (fn () =>
    2.13 +                #equiv_thm (the (Quotient_Info.lookup_quotients lthy typ_name)) 
    2.14 +                  RS @{thm Equiv_Relations.equivp_reflp} RS thm) ()
    2.15              | _ => NONE
    2.16              )
    2.17            | _ => NONE

     3.1 --- a/src/HOL/Word/WordBitwise.thy	Tue Jan 15 16:34:19 2013 +0100
     3.2 +++ b/src/HOL/Word/WordBitwise.thy	Tue Jan 15 17:28:46 2013 +0100
     3.3 @@ -514,10 +514,12 @@
     3.4        |> mk_nat_clist;
     3.5      val prop = Thm.mk_binop @{cterm "op = :: nat list => _"} ct ns
     3.6                   |> Thm.apply @{cterm Trueprop};
     3.7 -  in Goal.prove_internal [] prop 
     3.8 -      (K (REPEAT_DETERM (resolve_tac @{thms upt_eq_list_intros} 1
     3.9 -          ORELSE simp_tac word_ss 1))) |> mk_meta_eq |> SOME end
    3.10 -    handle TERM _ => NONE
    3.11 +  in
    3.12 +    try (fn () =>
    3.13 +      Goal.prove_internal [] prop 
    3.14 +        (K (REPEAT_DETERM (resolve_tac @{thms upt_eq_list_intros} 1
    3.15 +            ORELSE simp_tac word_ss 1))) |> mk_meta_eq) ()
    3.16 +  end
    3.17    | _ => NONE;
    3.18  
    3.19  val expand_upt_simproc = Simplifier.make_simproc