# HG changeset patch
# User wenzelm
# Date 1702294062 -3600
# Node ID 9cb8053d720eab0fac1068ac1d045874422950ef
# Parent  1f59664dab5170bb5bdaca815faf2b446d2e6664
clarified signature;

diff -r 1f59664dab51 -r 9cb8053d720e src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Dec 11 12:06:18 2023 +0100
+++ b/src/Pure/proofterm.ML	Mon Dec 11 12:27:42 2023 +0100
@@ -131,8 +131,8 @@
   val lift_proof: term -> int -> term list -> proof -> proof
   val incr_indexes: int -> proof -> proof
   val assumption_proof: term list -> term -> int -> proof -> proof
-  val bicompose_proof: bool -> term list -> term list -> term option -> term list ->
-    int -> int -> proof -> proof -> proof
+  val bicompose_proof: Envir.env -> bool -> term list -> term list -> term option ->
+    term list -> int -> int -> proof -> proof -> proof
   val reflexive_axm: proof
   val symmetric_axm: proof
   val transitive_axm: proof
@@ -1079,12 +1079,14 @@
   | flatten_params_proof i j n (_, k) = proof_combP (proof_combt (PBound (k+i),
       map Bound (j-1 downto 0)), map PBound (remove (op =) (i-n) (i-1 downto 0)));
 
-fun bicompose_proof flatten Bs As A oldAs n m rprf sprf =
+fun bicompose_proof env flatten Bs As A oldAs n m rprf sprf =
   let
+    val normt = Envir.norm_term env;
+
     val lb = length Bs;
     val la = length As;
   in
-    mk_AbsP (Bs @ As) (proof_combP (sprf,
+    mk_AbsP (map normt (Bs @ As)) (proof_combP (sprf,
       map PBound (lb + la - 1 downto la)) %%
         proof_combP (rprf, (if n>0 then [mk_asm_prf (the A) n m] else []) @
           map (if flatten then flatten_params_proof 0 0 n else PBound o snd)
diff -r 1f59664dab51 -r 9cb8053d720e src/Pure/thm.ML
--- 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