# HG changeset patch
# User kuncar
# Date 1430567886 -7200
# Node ID 8657416869269e8e02f014852c768826fcaa1df5
# Parent  3cab6f891c2faa07bf0e5f6f48dbf9af27fa2446
handle error messages also in after_qed

diff -r 3cab6f891c2f -r 865741686926 src/HOL/Tools/Lifting/lifting_def_code_dt.ML
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Sat May 02 13:58:06 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Sat May 02 13:58:06 2015 +0200
@@ -734,6 +734,28 @@
     error error_msg
   end
 
+fun check_rty_err ctxt (rty_schematic, rty_forced) (raw_var, rhs_raw) =
+  let
+    val (_, ctxt') = yield_singleton Proof_Context.read_vars raw_var ctxt
+    val rhs = (Syntax.check_term ctxt' o Syntax.parse_term ctxt') rhs_raw
+    val error_msg = cat_lines
+       ["Lifting failed for the following term:",
+        Pretty.string_of (Pretty.block
+         [Pretty.str "Term:", Pretty.brk 2, Syntax.pretty_term ctxt rhs]),
+        Pretty.string_of (Pretty.block
+         [Pretty.str "Type:", Pretty.brk 2, Syntax.pretty_typ ctxt rty_schematic]),
+        "",
+        (Pretty.string_of (Pretty.block
+         [Pretty.str "Reason:",
+          Pretty.brk 2,
+          Pretty.str "The type of the term cannot be instantiated to",
+          Pretty.brk 1,
+          Pretty.quote (Syntax.pretty_typ ctxt rty_forced),
+          Pretty.str "."]))]
+    in
+      error error_msg
+    end
+
 fun lift_def_cmd (params, raw_var, rhs_raw, par_xthms) lthy =
   let
     val config = evaluate_params params
@@ -761,33 +783,15 @@
               end
           in
             (SOME readable_rsp_tm_tnames, after_qed')
-          end 
+          end
+    fun after_qed_with_err_handling thmss ctxt = (after_qed thmss ctxt
+      handle Lifting_Term.QUOT_THM (rty, qty, msg) => quot_thm_err lthy (rty, qty) msg)
+      handle Lifting_Term.CHECK_RTY (rty_schematic, rty_forced) =>
+        check_rty_err lthy (rty_schematic, rty_forced) (raw_var, rhs_raw);
   in
-    Proof.theorem NONE (snd oo after_qed) [map (rpair []) (the_list goal)] lthy
+    Proof.theorem NONE (snd oo after_qed_with_err_handling) [map (rpair []) (the_list goal)] lthy
   end
 
-fun check_rty_err ctxt (rty_schematic, rty_forced) (raw_var, rhs_raw) =
-  let
-    val (_, ctxt') = yield_singleton Proof_Context.read_vars raw_var ctxt
-    val rhs = (Syntax.check_term ctxt' o Syntax.parse_term ctxt') rhs_raw
-    val error_msg = cat_lines
-       ["Lifting failed for the following term:",
-        Pretty.string_of (Pretty.block
-         [Pretty.str "Term:", Pretty.brk 2, Syntax.pretty_term ctxt rhs]),
-        Pretty.string_of (Pretty.block
-         [Pretty.str "Type:", Pretty.brk 2, Syntax.pretty_typ ctxt rty_schematic]),
-        "",
-        (Pretty.string_of (Pretty.block
-         [Pretty.str "Reason:",
-          Pretty.brk 2,
-          Pretty.str "The type of the term cannot be instantiated to",
-          Pretty.brk 1,
-          Pretty.quote (Syntax.pretty_typ ctxt rty_forced),
-          Pretty.str "."]))]
-    in
-      error error_msg
-    end
-
 fun lift_def_cmd_with_err_handling (params, (raw_var, rhs_raw, par_xthms)) lthy =
   (lift_def_cmd (params, raw_var, rhs_raw, par_xthms) lthy
     handle Lifting_Term.QUOT_THM (rty, qty, msg) => quot_thm_err lthy (rty, qty) msg)