# HG changeset patch
# User wenzelm
# Date 1702046266 -3600
# Node ID f991d3003ec8c6c85063f8d3b8c3240d45f94266
# Parent  59a70d1e1b140c968084c175693a99a1eee44a0d
more zproofs;

diff -r 59a70d1e1b14 -r f991d3003ec8 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Dec 08 15:30:53 2023 +0100
+++ b/src/Pure/thm.ML	Fri Dec 08 15:37:46 2023 +0100
@@ -1663,9 +1663,11 @@
               val prop' = Envir.norm_term env prop;
               val thy' = Context.certificate_theory cert' handle ERROR msg =>
                 raise CONTEXT (msg, [], [], [th], Option.map Context.Proof opt_ctxt);
-              val der' = deriv_rule1 (Proofterm.norm_proof_remove_types env, ZTerm.todo_proof) der;
+
+              fun prf p = Proofterm.norm_proof_remove_types env p;
+              fun zprf p = ZTerm.norm_proof thy' env p;
             in
-              Thm (der',
+              Thm (deriv_rule1 (prf, zprf) der,
                {cert = cert',
                 tags = [],
                 maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop'),