proper proof_serial;
authorwenzelm
Fri, 26 Jul 2019 09:50:23 +0200
changeset 70599 dc65ea294736
parent 70598 913b4afb6ac2
child 70600 3c20a86f14f1
proper proof_serial;
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),