# 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]));