# HG changeset patch
# User wenzelm
# Date 1702047488 -3600
# Node ID b7b231eceb62098f94b4cb2aa1c60aa6feff438d
# Parent  f991d3003ec8c6c85063f8d3b8c3240d45f94266
tuned: avoid shadowing;

diff -r f991d3003ec8 -r b7b231eceb62 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Dec 08 15:37:46 2023 +0100
+++ b/src/Pure/proofterm.ML	Fri Dec 08 15:58:08 2023 +0100
@@ -1057,14 +1057,14 @@
 
 (* proof by assumption *)
 
-fun mk_asm_prf t i m =
+fun mk_asm_prf C i m =
   let
     fun imp_prf _ i 0 = PBound i
       | imp_prf (Const ("Pure.imp", _) $ A $ B) i m = AbsP ("H", NONE (*A*), imp_prf B (i+1) (m-1))
       | imp_prf _ i _ = PBound i;
     fun all_prf (Const ("Pure.all", _) $ Abs (a, T, t)) = Abst (a, NONE (*T*), all_prf t)
       | all_prf t = imp_prf t (~i) m
-  in all_prf t end;
+  in all_prf C end;
 
 fun assumption_proof Bs Bi n prf =
   mk_AbsP Bs (proof_combP (prf, map PBound (length Bs - 1 downto 0) @ [mk_asm_prf Bi n ~1]));