tuned signature;

--- a/src/Pure/Proof/extraction.ML	Fri Jul 12 14:18:56 2024 +0200
+++ b/src/Pure/Proof/extraction.ML	Sun Jul 14 15:16:08 2024 +0200
@@ -188,7 +188,7 @@
        {oracles = Ord_List.make Proofterm.oracle_ord oracles,
         thms = Ord_List.make Proofterm.thm_ord thms,
         zboxes = [],
-        zproof = ZDummy,
+        zproof = ZNop,
         proof = prf};
   in Proofterm.thm_body body end;
 

--- a/src/Pure/proofterm.ML	Fri Jul 12 14:18:56 2024 +0200
+++ b/src/Pure/proofterm.ML	Sun Jul 14 15:16:08 2024 +0200
@@ -336,7 +336,7 @@
 
 fun no_proof_body zproof proof =
   PBody {oracles = [], thms = [], zboxes = [], zproof = zproof, proof = proof};
-val no_thm_body = thm_body (no_proof_body ZDummy MinProof);
+val no_thm_body = thm_body (no_proof_body ZNop MinProof);
 
 fun no_thm_names (Abst (x, T, prf)) = Abst (x, T, no_thm_names prf)
   | no_thm_names (AbsP (x, t, prf)) = AbsP (x, t, no_thm_names prf)
@@ -459,7 +459,7 @@
     val (a, b, c) =
       triple (list (pair (pair string (Position.of_properties o properties))
         (option (term consts)))) (list (thm consts)) (proof consts) x;
-  in PBody {oracles = a, thms = b, zboxes = [], zproof = ZDummy, proof = c} end
+  in PBody {oracles = a, thms = b, zboxes = [], zproof = ZNop, proof = c} end
 and thm consts x =
   let
     val (a, (b, (c, (d, e)))) =
@@ -2187,7 +2187,7 @@
     val (zproof1, zboxes1) =
       if zproof_enabled proofs then
         ZTerm.add_box_proof {unconstrain = unconstrain} thy hyps concl zproof0 zboxes0
-      else (ZDummy, []);
+      else (ZNop, []);
     val proof1 =
       if proof_enabled proofs then fold_rev implies_intr_proof hyps proof0
       else MinProof;
@@ -2198,7 +2198,7 @@
         val unconstrainT = unconstrainT_proof (Sign.classes_of thy) sorts_proof ucontext;
         val postproc = map_proof_of (unconstrainT #> named ? rew_proof thy);
         val body1 =
-          {oracles = oracles0, thms = thms0, zboxes = [], zproof = ZDummy, proof = proof1};
+          {oracles = oracles0, thms = thms0, zboxes = [], zproof = ZNop, proof = proof1};
       in (i, fulfill_proof_future thy promises postproc (Future.value (PBody body1))) end;
 
     val (i, body') =

--- a/src/Pure/thm.ML	Fri Jul 12 14:18:56 2024 +0200
+++ b/src/Pure/thm.ML	Sun Jul 14 15:16:08 2024 +0200
@@ -757,7 +757,7 @@
   make_deriv0 promises
     (PBody {oracles = oracles, thms = thms, zboxes = zboxes, zproof = zproof, proof = proof});
 
-val empty_deriv = make_deriv [] [] [] [] ZDummy MinProof;
+val empty_deriv = make_deriv [] [] [] [] ZNop MinProof;
 
 
 (* inference rules *)
@@ -778,7 +778,7 @@
     val zboxes' = ZTerm.union_zboxes zboxes1 zboxes2;
 
     val proofs = Proofterm.get_proofs_level ();
-    val zproof' = if Proofterm.zproof_enabled proofs then zproof zprf1 zprf2 else ZDummy;
+    val zproof' = if Proofterm.zproof_enabled proofs then zproof zprf1 zprf2 else ZNop;
     val proof' = if Proofterm.proof_enabled proofs then proof prf1 prf2 else MinProof;
   in make_deriv ps' oracles' thms' zboxes' zproof' proof' end;
 
@@ -788,7 +788,7 @@
   let val proofs = Proofterm.get_proofs_level () in
     if Proofterm.proof_enabled proofs orelse Proofterm.zproof_enabled proofs then
       deriv_rule1 I I (make_deriv [] [] [] []
-       (if Proofterm.zproof_enabled proofs then zproof () else ZDummy)
+       (if Proofterm.zproof_enabled proofs then zproof () else ZNop)
        (if Proofterm.proof_enabled proofs then proof () else MinProof))
     else empty_deriv
   end;
@@ -853,7 +853,7 @@
     val i = serial ();
     val future = future_thm |> Future.map (future_result i cert sorts prop);
   in
-    Thm (make_deriv [(i, future)] [] [] [] ZDummy MinProof,
+    Thm (make_deriv [(i, future)] [] [] [] ZNop MinProof,
      {cert = cert,
       tags = [],
       maxidx = maxidx,
@@ -1203,7 +1203,7 @@
                   val thy = Context.certificate_theory cert handle ERROR msg =>
                     raise CONTEXT (msg, [], [ct], [], NONE);
                 in ZTerm.oracle_proof thy name prop end
-              else ZDummy;
+              else ZNop;
           in
             Thm (make_deriv [] [oracle] [] [] zproof proof,
              {cert = cert,
@@ -2115,7 +2115,7 @@
       raise THM ("store_zproof: theorem may not use promises", 0, [thm]);
 
     val ((i, (_, zproof1)), zproof2) = ZTerm.thm_proof thy name hyps prop zproof;
-    val der1 = if Options.default_bool "prune_proofs" then deriv [] ZDummy else deriv zboxes zproof1;
+    val der1 = if Options.default_bool "prune_proofs" then deriv [] ZNop else deriv zboxes zproof1;
     val der2 = deriv [] zproof2;
 
     val thm' = trim_context (Thm (der1, args));

--- a/src/Pure/zterm.ML	Fri Jul 12 14:18:56 2024 +0200
+++ b/src/Pure/zterm.ML	Sun Jul 14 15:16:08 2024 +0200
@@ -200,7 +200,7 @@
 type zproof_const = (zproof_name * zterm) * (ztyp ZTVars.table * zterm ZVars.table);
 
 datatype zproof =
-    ZDummy                         (*dummy proof*)
+    ZNop
   | ZConstp of zproof_const
   | ZBoundp of int
   | ZAbst of string * ztyp * zproof
@@ -480,7 +480,7 @@
 
 fun fold_proof {hyps} typ term =
   let
-    fun proof ZDummy = I
+    fun proof ZNop = I
       | proof (ZConstp (_, (instT, inst))) =
           ZTVars.fold (typ o #2) instT #> ZVars.fold (term o #2) inst
       | proof (ZBoundp _) = I
@@ -538,7 +538,7 @@
 
 fun map_proof_same {hyps} typ term =
   let
-    fun proof ZDummy = raise Same.SAME
+    fun proof ZNop = raise Same.SAME
       | proof (ZConstp (a, (instT, inst))) =
           ZConstp (a, map_insts_same typ term (instT, inst))
       | proof (ZBoundp _) = raise Same.SAME