Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/thm.ML
changeset 79261 2e6fcc331f10
parent 79260 f4067f14c9ed
child 79262 64c655e8e8bf 
--- a/src/Pure/thm.ML	Wed Dec 13 19:58:26 2023 +0100
+++ b/src/Pure/thm.ML	Wed Dec 13 23:05:41 2023 +0100
@@ -2372,7 +2372,8 @@
         val constraints' =
           union_constraints constraints1 constraints2
           |> insert_constraints_env thy' env;
-        fun zproof p q = ZTerm.todo_proof p;
+        fun zproof p q =
+          ZTerm.bicompose_proof thy' env smax flatten Bs As A oldAs n (nlift + 1) p q;
         fun proof p q =
           Proofterm.bicompose_proof env smax flatten Bs As A oldAs n (nlift + 1) p q;
         val th =
isabelle