# HG changeset patch
# User wenzelm
# Date 1683800510 -7200
# Node ID 9c18535a9fcd121c6309e106cf6ec97b43b37f3e
# Parent  73c77db63594a94b0d801734fe2d7239e2e6d621
proper exception CONTEXT for Context.certificate_theory;

diff -r 73c77db63594 -r 9c18535a9fcd src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu May 11 12:20:47 2023 +0200
+++ b/src/Pure/thm.ML	Thu May 11 12:21:50 2023 +0200
@@ -992,7 +992,8 @@
       let
         val {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop} = args;
 
-        val thy = Context.certificate_theory cert;
+        val thy = Context.certificate_theory cert
+          handle ERROR msg => raise CONTEXT (msg, [], [], [thm], NONE);
         val bad_thys =
           constraints |> map_filter (fn {theory = thy', ...} =>
             if Context.eq_thy (thy, thy') then NONE else SOME thy');
@@ -1558,8 +1559,9 @@
                 (*remove trivial tpairs, of the form t \<equiv> t*)
                 |> filter_out (op aconv);
               val der' = deriv_rule1 (Proofterm.norm_proof' env) der;
-              val constraints' =
-                insert_constraints_env (Context.certificate_theory cert') env constraints;
+              val thy' = Context.certificate_theory cert' handle ERROR msg =>
+                raise CONTEXT (msg, [], [], [th], Option.map Context.Proof opt_ctxt);
+              val constraints' = insert_constraints_env thy' env constraints;
               val prop' = Envir.norm_term env prop;
               val maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop');
               val shyps = Envir.insert_sorts env shyps;
@@ -1699,7 +1701,8 @@
       val (tpairs', maxidx') =
         fold_map (fn (t, u) => fn i => subst t i ||>> subst u) tpairs maxidx1;
 
-      val thy' = Context.certificate_theory cert';
+      val thy' = Context.certificate_theory cert'
+        handle ERROR msg => raise CONTEXT (msg, [], [], [th], NONE);
       val constraints' =
         TVars.fold (fn ((_, S), (T, _)) => insert_constraints thy' (T, S))
           instT' constraints;
@@ -1927,12 +1930,14 @@
         val normt = Envir.norm_term env;
         fun assumption_proof prf =
           Proofterm.assumption_proof (map normt Bs) (normt Bi) n prf;
+        val thy' = Context.certificate_theory cert' handle ERROR msg =>
+          raise CONTEXT (msg, [], [], [state], Option.map Context.Proof opt_ctxt);
       in
         Thm (deriv_rule1
           (assumption_proof #> not (Envir.is_empty env) ? Proofterm.norm_proof' env) der,
          {tags = [],
           maxidx = Envir.maxidx_of env,
-          constraints = insert_constraints_env (Context.certificate_theory cert') env constraints,
+          constraints = insert_constraints_env thy' env constraints,
           shyps = Envir.insert_sorts env shyps,
           hyps = hyps,
           tpairs = if Envir.is_empty env then tpairs else map (apply2 normt) tpairs,
@@ -2174,9 +2179,11 @@
                 else (*normalize the new rule fully*)
                   (ntps, (map normt (Bs @ As), normt C))
              end
+           val thy' = Context.certificate_theory cert handle ERROR msg =>
+            raise CONTEXT (msg, [], [], [state, orule], Option.map Context.Proof opt_ctxt);
            val constraints' =
              union_constraints constraints1 constraints2
-             |> insert_constraints_env (Context.certificate_theory cert) env;
+             |> insert_constraints_env thy' env;
            fun bicompose_proof prf1 prf2 =
              Proofterm.bicompose_proof flatten (map normt Bs) (map normt As) A oldAs n (nlift+1)
                prf1 prf2