tuned;

--- a/src/Pure/proofterm.ML	Sun Jul 21 13:04:01 2024 +0200
+++ b/src/Pure/proofterm.ML	Sun Jul 21 13:44:05 2024 +0200
@@ -397,7 +397,7 @@
       | zproof (PAxm (a, prop, SOME Ts)) = zproof_const (ZAxiom a) prop Ts
       | zproof (PClass (T, c)) = OFCLASSp (ztyp T, c)
       | zproof (Oracle (a, prop, SOME Ts)) = zproof_const (ZOracle a) prop Ts
-      | zproof (PThm ({serial, command_pos, theory_name, thm_name, prop, types = SOME Ts, ...}, _)) =
+      | zproof (PThm ({serial, theory_name, thm_name, prop, types = SOME Ts, ...}, _)) =
           let val proof_name =
             ZThm {theory_name = theory_name, thm_name = thm_name, serial = serial};
           in zproof_const proof_name prop Ts end;