# 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 "