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 79240 9cb8053d720e
parent 79239 1f59664dab51
child 79241 a49bdb686545 
--- a/src/Pure/thm.ML	Mon Dec 11 12:06:18 2023 +0100
+++ b/src/Pure/thm.ML	Mon Dec 11 12:27:42 2023 +0100
@@ -2348,7 +2348,7 @@
           |> insert_constraints_env thy' env;
         fun zproof p q = ZTerm.todo_proof p;
         fun bicompose_proof p q =
-          Proofterm.bicompose_proof flatten (map normt Bs) (map normt As) A oldAs n (nlift+1) p q;
+          Proofterm.bicompose_proof env flatten Bs As A oldAs n (nlift+1) p q;
         val proof =
           if Envir.is_empty env then bicompose_proof
           else if Envir.above env smax
isabelle