# HG changeset patch
# User wenzelm
# Date 1721411840 -7200
# Node ID 839c4f8742f9ddfc86fec339f885f87e6f5ec970
# Parent  1d6e5b7a6906c2bf905df2f51f39c8d415c41b0f
more predictable proof id;

diff -r 1d6e5b7a6906 -r 839c4f8742f9 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Jul 19 17:58:13 2024 +0200
+++ b/src/Pure/proofterm.ML	Fri Jul 19 19:57:20 2024 +0200
@@ -206,6 +206,8 @@
 
 (** datatype proof **)
 
+val proof_serial = Counter.make ();
+
 type thm_header =
   {serial: serial, command_pos: Position.T, theory_name: string, thm_name: Thm_Name.P,
     prop: term, types: typ list option};
@@ -2210,7 +2212,7 @@
 
     fun new_prf () =
       let
-        val i = serial ();
+        val i = proof_serial ();
         val unconstrainT = unconstrainT_proof (Sign.classes_of thy) sorts_proof ucontext;
         val postproc = map_proof_of (unconstrainT #> named ? rew_proof thy);
         val body1 =
@@ -2226,7 +2228,7 @@
             if (#1 a = "" orelse a = name) andalso prop' = prop1 andalso args' = args then
               let
                 val Thm_Body {body = body', ...} = thm_body';
-                val i = if #1 a = "" andalso named then serial () else ser;
+                val i = if #1 a = "" andalso named then proof_serial () else ser;
               in (i, body' |> ser <> i ? Future.map (map_proof_of (rew_proof thy))) end
             else new_prf ()
         | _ => new_prf ());