# HG changeset patch
# User wenzelm
# Date 1563967815 -7200
# Node ID f881efa6be5008754c1dc7214891127e30a50792
# Parent  be32cb8bfe2574b9f85aca89904c2b6656e6af25
prefer local counter;

diff -r be32cb8bfe25 -r f881efa6be50 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Wed Jul 24 13:19:00 2019 +0200
+++ b/src/Pure/proofterm.ML	Wed Jul 24 13:30:15 2019 +0200
@@ -1688,6 +1688,8 @@
 
 (** theorems **)
 
+val proof_serial = Counter.make ();
+
 fun prepare_thm_proof thy name shyps hyps concl promises body =
   let
     val PBody {oracles = oracles0, thms = thms0, proof = prf} = body;
@@ -1731,7 +1733,7 @@
 
     fun new_prf () =
       let
-        val i = serial ();
+        val i = proof_serial ();
         val postproc =
           unconstrainT_body thy (atyp_map, constraints) #>
           name <> "" ? map_proof_of (clean_proof thy #> publish i);