# HG changeset patch
# User wenzelm
# Date 1702291850 -3600
# Node ID 42b2177a9d19c8ca098c3c6eff3ed847bba26479
# Parent  f97fe7ad62a7f2894aa7e9e9cf0d69c708acbe47
tuned;

diff -r f97fe7ad62a7 -r 42b2177a9d19 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Dec 11 11:46:12 2023 +0100
+++ b/src/Pure/thm.ML	Mon Dec 11 11:50:50 2023 +0100
@@ -2375,7 +2375,7 @@
              fun proof p = Proofterm.map_proof_terms (rename K) I p;
              fun zproof p = ZTerm.todo_proof p;
            in (map (rename strip_apply) As0, deriv_rule1 zproof proof rder) end;
-       in (map (if flatten then (Logic.flatten_params n) else I) As1, As1, rder', n)
+       in (if flatten then map (Logic.flatten_params n) As1 else As1, As1, rder', n)
           handle TERM _ =>
           raise THM("bicompose: 1st premise", 0, [orule])
        end;