--- 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)
--- 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