# HG changeset patch
# User haftmann
# Date 1465241326 -7200
# Node ID f82c0b803bda6d62c7f1943b52e6944b3f2a0347
# Parent  d562c9948deec004145b39be77b8397d3eb3047a
more correct exception handling

diff -r d562c9948dee -r f82c0b803bda src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Mon Jun 06 21:28:46 2016 +0200
+++ b/src/Pure/Isar/code.ML	Mon Jun 06 21:28:46 2016 +0200
@@ -513,7 +513,7 @@
       | _ => ();
   in () end;
 
-fun gen_assert_eqn thy check_patterns (thm, proper) =
+fun assert_eqn' thy check_patterns (thm, proper) =
   let
     val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
       handle TERM _ => bad_thm "Not an equation"
@@ -522,7 +522,7 @@
       allow_consts = not (proper andalso check_patterns), allow_pats = true } thm (lhs, rhs);
   in (thm, proper) end;
 
-fun assert_abs_eqn thy some_tyco thm =
+fun assert_abs_eqn' thy some_tyco thm =
   let
     val (full_lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
       handle TERM _ => bad_thm "Not an equation"
@@ -548,27 +548,29 @@
       else error ("Type arguments do not satisfy sort constraints of abstype certificate.");
   in (thm, tyco) end;
 
-fun assert_eqn thy = gen_assert_eqn thy true;
+fun assert_eqn thy = error_thm (assert_eqn' thy true) thy;
+
+fun assert_abs_eqn thy some_tyco = error_abs_thm (assert_abs_eqn' thy some_tyco) thy;
 
 fun meta_rewrite thy = Local_Defs.meta_rewrite_rule (Proof_Context.init_global thy);
 
-fun mk_eqn thy = error_thm (gen_assert_eqn thy false) thy o
+fun mk_eqn thy = error_thm (assert_eqn' thy false) thy o
   apfst (meta_rewrite thy);
 
 fun mk_eqn_liberal thy = Option.map (fn (thm, _) => (thm, is_linear thm))
-  o try_thm (gen_assert_eqn thy false) o rpair false o meta_rewrite thy;
+  o try_thm (assert_eqn' thy false) o rpair false o meta_rewrite thy;
 
 fun mk_eqn_maybe_abs thy raw_thm =
   let
     val thm = meta_rewrite thy raw_thm;
-    val some_abs_thm = try_thm (assert_abs_eqn thy NONE) thm;
+    val some_abs_thm = try_thm (assert_abs_eqn' thy NONE) thm;
   in case some_abs_thm
    of SOME (thm, tyco) => SOME ((thm, true), SOME tyco)
     | NONE => (Option.map (fn (thm, _) => ((thm, is_linear thm), NONE))
-        o warning_thm (gen_assert_eqn thy false) thy) (thm, false)
+        o warning_thm (assert_eqn' thy false) thy) (thm, false)
   end;
 
-fun mk_abs_eqn thy = error_abs_thm (assert_abs_eqn thy NONE) thy o meta_rewrite thy;
+fun mk_abs_eqn thy = error_abs_thm (assert_abs_eqn' thy NONE) thy o meta_rewrite thy;
 
 val head_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
 
@@ -753,7 +755,7 @@
       let
         val thy = Proof_Context.theory_of ctxt;
         val eqns = burrow_fst (canonize_thms thy) raw_eqns;
-        val _ = map (error_thm (assert_eqn thy) thy) eqns;
+        val _ = map (assert_eqn thy) eqns;
         val (thms, propers) = split_list eqns;
         val _ = map (fn thm => if c = const_eqn thy thm then ()
           else error ("Wrong head of code equation,\nexpected constant "