Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
proper proof_serial;
authorwenzelm
Fri, 26 Jul 2019 09:50:23 +0200
changeset 70414 dc65ea294736
parent 70413 913b4afb6ac2
child 70415 3c20a86f14f1
proper proof_serial;
src/Pure/Proof/extraction.ML file | annotate | diff | comparison | revisions 
--- 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),
isabelle