changeset 79315 | 140c7fac037a |
parent 79313 | 3b03af5125de |
child 79318 | 74e245625a67 |
--- a/src/Pure/zterm.ML Tue Dec 19 23:06:26 2023 +0100 +++ b/src/Pure/zterm.ML Wed Dec 20 11:16:39 2023 +0100 @@ -746,7 +746,7 @@ | _ => tab))); in (a, A, instT, inst) end; -fun make_const_proof (f, g) ((a, A, instT, inst): zproof_const) = +fun make_const_proof (f, g) (a, A, instT, inst) = let val instT' = ZTVars.map (fn ((x, _), _) => fn y => the_default y (try f x)) instT; val inst' = ZVars.map (fn ((x, _), _) => fn y => the_default y (try g x)) inst;