# HG changeset patch
# User wenzelm
# Date 1564127423 -7200
# Node ID dc65ea2947365564330545fa7e66276cd8585806
# Parent  913b4afb6ac20ac8a73937a97a73d48e30b35ac8
proper proof_serial;

diff -r 913b4afb6ac2 -r dc65ea294736 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Fri Jul 26 09:50:12 2019 +0200
+++ b/src/Pure/Proof/extraction.ML	Fri Jul 26 09:50:23 2019 +0200
@@ -623,7 +623,7 @@
                     val corr_prop = Reconstruct.prop_of corr_prf;
                     val corr_prf' =
                       Proofterm.proof_combP (Proofterm.proof_combt
-                         (PThm (serial (),
+                         (PThm (Proofterm.proof_serial (),
                           ((corr_name name vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev)), I),
                             Future.value (Proofterm.approximate_proof_body corr_prf))),
                               vfs_of corr_prop),
@@ -740,7 +740,7 @@
                     val corr_prop = Reconstruct.prop_of corr_prf';
                     val corr_prf'' =
                       Proofterm.proof_combP (Proofterm.proof_combt
-                        (PThm (serial (),
+                        (PThm (Proofterm.proof_serial (),
                          ((corr_name s vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev)), I),
                            Future.value (Proofterm.approximate_proof_body corr_prf'))),
                             vfs_of corr_prop),