# HG changeset patch
# User wenzelm
# Date 1703100535 -3600
# Node ID dbfe6d1fdfb6ee8d6a95f1594de8551cb26ae64d
# Parent  bbac3e8a50708c31a7b9db191f501cc6900add71
more informative exceptions;

diff -r bbac3e8a5070 -r dbfe6d1fdfb6 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Dec 20 14:26:18 2023 +0100
+++ b/src/Pure/thm.ML	Wed Dec 20 20:28:55 2023 +0100
@@ -1154,7 +1154,7 @@
     val (name, oracles') = Name_Space.define (Context.Theory thy) true (b, ()) (get_oracles thy);
     val thy' = map_oracles (K oracles') thy;
     fun invoke_oracle arg =
-      let val Cterm {cert = cert2, t = prop, T, maxidx, sorts} = oracle_fn arg in
+      let val ct as Cterm {cert = cert2, t = prop, T, maxidx, sorts} = oracle_fn arg in
         if T <> propT then
           raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
         else
@@ -1170,8 +1170,11 @@
               then Proofterm.oracle_proof name prop
               else MinProof;
             val zproof =
-              if Proofterm.zproof_enabled proofs
-              then ZTerm.oracle_proof (Context.certificate_theory cert) name prop
+              if Proofterm.zproof_enabled proofs then
+                let
+                  val thy'' = Context.certificate_theory cert handle ERROR msg =>
+                    raise CONTEXT (msg, [], [ct], [], SOME (Context.Theory thy'));
+                in ZTerm.oracle_proof thy'' name prop end
               else ZDummy;
           in
             Thm (make_deriv [] [oracle] [] [] zproof proof,
@@ -1206,14 +1209,18 @@
 
 (*The assumption rule A |- A*)
 fun assume raw_ct =
-  let val Cterm {cert, t = prop, T, maxidx, sorts} = adjust_maxidx_cterm ~1 raw_ct in
+  let val ct as Cterm {cert, t = prop, T, maxidx, sorts} = adjust_maxidx_cterm ~1 raw_ct in
     if T <> propT then
       raise THM ("assume: prop", 0, [])
     else if maxidx <> ~1 then
       raise THM ("assume: variables", maxidx, [])
     else
       let
-        fun zproof () = ZTerm.assume_proof (Context.certificate_theory cert) prop;
+        fun zproof () =
+          let
+            val thy = Context.certificate_theory cert handle ERROR msg =>
+              raise CONTEXT (msg, [], [ct], [], NONE);
+          in ZTerm.assume_proof thy prop end;
         fun proof () = Proofterm.Hyp prop;
       in
         Thm (deriv_rule0 zproof proof,
@@ -1243,7 +1250,11 @@
   else
     let
       val cert = join_certificate1 (ct, th);
-      fun zproof p = ZTerm.implies_intr_proof (Context.certificate_theory cert) A p;
+      fun zproof p =
+        let
+          val thy = Context.certificate_theory cert handle ERROR msg =>
+            raise CONTEXT (msg, [], [ct], [th], NONE);
+        in ZTerm.implies_intr_proof thy A p end
       fun proof p = Proofterm.implies_intr_proof A p;
     in
       Thm (deriv_rule1 zproof proof der,
@@ -1308,7 +1319,11 @@
       else
         let
           val cert = join_certificate1 (ct, th);
-          fun zproof p = ZTerm.forall_intr_proof (Context.certificate_theory cert) T (a, x) p;
+          fun zproof p =
+            let
+              val thy = Context.certificate_theory cert handle ERROR msg =>
+                raise CONTEXT (msg, [], [ct], [th], NONE);
+            in ZTerm.forall_intr_proof thy T (a, x) p end;
           fun proof p = Proofterm.forall_intr_proof (a, x) NONE p;
         in
           Thm (deriv_rule1 zproof proof der,
@@ -1343,7 +1358,11 @@
       else
         let
           val cert = join_certificate1 (ct, th);
-          fun zproof p = ZTerm.forall_elim_proof (Context.certificate_theory cert) t p;
+          fun zproof p =
+            let
+              val thy = Context.certificate_theory cert handle ERROR msg =>
+                raise CONTEXT (msg, [], [ct], [th], NONE);
+            in ZTerm.forall_elim_proof thy t p end;
           fun proof p = p % SOME t;
         in
           Thm (deriv_rule1 zproof proof der,
@@ -1364,9 +1383,13 @@
 (*Reflexivity
   t \<equiv> t
 *)
-fun reflexive (Cterm {cert, t, T, maxidx, sorts}) =
+fun reflexive (ct as Cterm {cert, t, T, maxidx, sorts}) =
   let
-    fun zproof () = ZTerm.reflexive_proof (Context.certificate_theory cert) T t;
+    fun zproof () =
+      let
+        val thy = Context.certificate_theory cert handle ERROR msg =>
+          raise CONTEXT (msg, [], [ct], [], NONE);
+      in ZTerm.reflexive_proof thy T t end;
     fun proof () = Proofterm.reflexive_proof;
   in
     Thm (deriv_rule0 zproof proof,
@@ -1388,7 +1411,13 @@
 fun symmetric (th as Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...})) =
   (case prop of
     (eq as Const ("Pure.eq", Type ("fun", [T, _]))) $ t $ u =>
-      let fun zproof p = ZTerm.symmetric_proof (Context.certificate_theory cert) T t u p in
+      let
+        fun zproof p =
+          let
+            val thy = Context.certificate_theory cert handle ERROR msg =>
+              raise CONTEXT (msg, [], [], [th], NONE);
+          in ZTerm.symmetric_proof thy T t u p end;
+      in
         Thm (deriv_rule1 zproof Proofterm.symmetric_proof der,
          {cert = cert,
           tags = [],
@@ -1420,7 +1449,11 @@
         else
           let
             val cert = join_certificate2 (th1, th2);
-            fun zproof p q = ZTerm.transitive_proof (Context.certificate_theory cert) T t1 u t2 p q;
+            fun zproof p q =
+              let
+                val thy = Context.certificate_theory cert handle ERROR msg =>
+                  raise CONTEXT (msg, [], [], [th1, th2], NONE);
+              in ZTerm.transitive_proof thy T t1 u t2 p q end;
             fun proof p = Proofterm.transitive_proof T u p;
           in
             Thm (deriv_rule2 zproof proof der1 der2,
@@ -1440,14 +1473,18 @@
   (\<lambda>x. t) u \<equiv> t[u/x]
   fully beta-reduces the term if full = true
 *)
-fun beta_conversion full (Cterm {cert, t, T, maxidx, sorts}) =
+fun beta_conversion full (ct as Cterm {cert, t, T, maxidx, sorts}) =
   let
     val t' =
       if full then Envir.beta_norm t
       else
         (case t of Abs (_, _, bodt) $ u => subst_bound (u, bodt)
         | _ => raise THM ("beta_conversion: not a redex", 0, []));
-    fun zproof () = ZTerm.reflexive_proof (Context.certificate_theory cert) T t;
+    fun zproof () =
+      let
+        val thy = Context.certificate_theory cert handle ERROR msg =>
+          raise CONTEXT (msg, [], [ct], [], NONE);
+      in ZTerm.reflexive_proof thy T t end;
     fun proof () = Proofterm.reflexive_proof;
   in
     Thm (deriv_rule0 zproof proof,
@@ -1461,9 +1498,13 @@
       prop = Logic.mk_equals (t, t')})
   end;
 
-fun eta_conversion (Cterm {cert, t, T, maxidx, sorts}) =
+fun eta_conversion (ct as Cterm {cert, t, T, maxidx, sorts}) =
   let
-    fun zproof () = ZTerm.reflexive_proof (Context.certificate_theory cert) T t;
+    fun zproof () =
+      let
+        val thy = Context.certificate_theory cert handle ERROR msg =>
+          raise CONTEXT (msg, [], [ct], [], NONE);
+      in ZTerm.reflexive_proof thy T t end;
     fun proof () = Proofterm.reflexive_proof;
   in
     Thm (deriv_rule0 zproof proof,
@@ -1477,9 +1518,13 @@
       prop = Logic.mk_equals (t, Envir.eta_contract t)})
   end;
 
-fun eta_long_conversion (Cterm {cert, t, T, maxidx, sorts}) =
+fun eta_long_conversion (ct as Cterm {cert, t, T, maxidx, sorts}) =
   let
-    fun zproof () = ZTerm.reflexive_proof (Context.certificate_theory cert) T t;
+    fun zproof () =
+      let
+        val thy = Context.certificate_theory cert handle ERROR msg =>
+          raise CONTEXT (msg, [], [ct], [], NONE);
+      in ZTerm.reflexive_proof thy T t end;
     fun proof () = Proofterm.reflexive_proof;
   in
     Thm (deriv_rule0 zproof proof,
@@ -1500,7 +1545,7 @@
   \<lambda>x. t \<equiv> \<lambda>x. u
 *)
 fun abstract_rule b
-    (Cterm {t = x, T, sorts, ...})
+    (ct as Cterm {t = x, T, sorts, ...})
     (th as Thm (der, {cert, maxidx, hyps, constraints, shyps, tpairs, prop, ...})) =
   let
     val (U, t, u) =
@@ -1515,7 +1560,10 @@
           val f = Abs (b, T, abstract_over (x, t));
           val g = Abs (b, T, abstract_over (x, u));
           fun zproof p =
-            ZTerm.abstract_rule_proof (Context.certificate_theory cert) T U (b, x) f g p;
+            let
+              val thy = Context.certificate_theory cert handle ERROR msg =>
+                raise CONTEXT (msg, [], [ct], [th], NONE);
+            in ZTerm.abstract_rule_proof thy T U (b, x) f g p end;
           fun proof p = Proofterm.abstract_rule_proof (b, x) p
         in
           Thm (deriv_rule1 zproof proof der,
@@ -1559,7 +1607,10 @@
             | _ => raise THM ("combination: not function type", 0, [th1, th2]));
           val cert = join_certificate2 (th1, th2);
           fun zproof p q =
-            ZTerm.combination_proof (Context.certificate_theory cert) fT U f g t u p q;
+            let
+              val thy = Context.certificate_theory cert handle ERROR msg =>
+                raise CONTEXT (msg, [], [], [th1, th2], NONE);
+            in ZTerm.combination_proof thy fT U f g t u p q end;
           fun proof p q = Proofterm.combination_proof f g t u p q;
         in
           Thm (deriv_rule2 zproof proof der1 der2,
@@ -1594,7 +1645,11 @@
           let
             val cert = join_certificate2 (th1, th2);
             fun proof p q = Proofterm.equal_intr_proof A B p q;
-            fun zproof p q = ZTerm.equal_intr_proof (Context.certificate_theory cert) A B p q;
+            fun zproof p q =
+              let
+                val thy = Context.certificate_theory cert handle ERROR msg =>
+                  raise CONTEXT (msg, [], [], [th1, th2], NONE);
+              in ZTerm.equal_intr_proof thy A B p q end;
           in
             Thm (deriv_rule2 zproof proof der1 der2,
              {cert = cert,
@@ -1629,7 +1684,11 @@
           let
             val cert = join_certificate2 (th1, th2);
             fun proof p q = Proofterm.equal_elim_proof A B p q;
-            fun zproof p q = ZTerm.equal_elim_proof (Context.certificate_theory cert) A B p q;
+            fun zproof p q =
+              let
+                val thy = Context.certificate_theory cert handle ERROR msg =>
+                  raise CONTEXT (msg, [], [], [th1, th2], NONE);
+              in ZTerm.equal_elim_proof thy A B p q end;
           in
             Thm (deriv_rule2 zproof proof der1 der2,
              {cert = cert,
@@ -1869,12 +1928,16 @@
 
 (*The trivial implication A \<Longrightarrow> A, justified by assume and forall rules.
   A can contain Vars, not so for assume!*)
-fun trivial (Cterm {cert, t = A, T, maxidx, sorts}) =
+fun trivial (ct as Cterm {cert, t = A, T, maxidx, sorts}) =
   if T <> propT then
     raise THM ("trivial: the term must have type prop", 0, [])
   else
     let
-      fun zproof () = ZTerm.trivial_proof (Context.certificate_theory cert) A;
+      fun zproof () =
+        let
+          val thy = Context.certificate_theory cert handle ERROR msg =>
+            raise CONTEXT (msg, [], [ct], [], NONE);
+        in ZTerm.trivial_proof thy A end;
       fun proof () = Proofterm.trivial_proof;
     in
       Thm (deriv_rule0 zproof proof,
@@ -2050,7 +2113,11 @@
       let
         val cert = join_certificate1 (goal, orule);
         val prems = map lift_all As;
-        fun zproof p = ZTerm.lift_proof (Context.certificate_theory cert) gprop inc prems p;
+        fun zproof p =
+          let
+            val thy = Context.certificate_theory cert
+              handle ERROR msg => raise CONTEXT (msg, [], [goal], [orule], NONE);
+          in ZTerm.lift_proof thy gprop inc prems p end;
         fun proof p = Proofterm.lift_proof gprop inc prems p;
       in
         Thm (deriv_rule1 zproof proof der,
@@ -2138,7 +2205,10 @@
     | n =>
         let
           fun zproof p =
-            ZTerm.assumption_proof (Context.certificate_theory cert) Envir.init Bs Bi (n + 1) [] p;
+            let
+              val thy = Context.certificate_theory cert
+                handle ERROR msg => raise CONTEXT (msg, [], [], [state], NONE);
+            in ZTerm.assumption_proof thy Envir.init Bs Bi (n + 1) [] p end;
           fun proof p = Proofterm.assumption_proof Bs Bi (n + 1) p;
         in
           Thm (deriv_rule1 zproof proof der,
@@ -2172,7 +2242,11 @@
         in Logic.list_all (params, Logic.list_implies (qs @ ps, concl)) end
       else raise THM ("rotate_rule", k, [state]);
 
-    fun zproof p = ZTerm.rotate_proof (Context.certificate_theory cert) Bs Bi' params asms m p;
+    fun zproof p =
+      let
+        val thy = Context.certificate_theory cert
+          handle ERROR msg => raise CONTEXT (msg, [], [], [state], NONE);
+      in ZTerm.rotate_proof thy Bs Bi' params asms m p end;
     fun proof p = Proofterm.rotate_proof Bs Bi' params asms m p;
   in
     Thm (deriv_rule1 zproof proof der,
@@ -2209,7 +2283,11 @@
         in (prems', Logic.list_implies (prems', concl)) end
       else raise THM ("permute_prems: k", k, [rl]);
 
-    fun zproof p = ZTerm.permute_prems_proof (Context.certificate_theory cert) prems' j m p;
+    fun zproof p =
+      let
+        val thy = Context.certificate_theory cert
+          handle ERROR msg => raise CONTEXT (msg, [], [], [rl], NONE);
+      in ZTerm.permute_prems_proof thy prems' j m p end;
     fun proof p = Proofterm.permute_prems_proof prems' j m p;
   in
     Thm (deriv_rule1 zproof proof der,