# HG changeset patch # User wenzelm # Date 1704229112 -3600 # Node ID 623789141e398598915309d5aaef835e1609f7be # Parent 740ec03b0b7129f613f72ca6c866a72223ca70f9 proper instantiation for make_const_proof, notably change of types for term variables; diff -r 740ec03b0b71 -r 623789141e39 src/Pure/zterm.ML --- a/src/Pure/zterm.ML Tue Jan 02 20:34:22 2024 +0100 +++ b/src/Pure/zterm.ML Tue Jan 02 21:58:32 2024 +0100 @@ -787,8 +787,9 @@ 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; + val typ = Same.function (fn ZTVar ((x, _), _) => try f x | _ => NONE); + val term = Same.function (fn ZVar ((x, _), _) => try g x | _ => NONE); + val (instT', inst') = Same.commit (map_insts_same typ term) (instT, inst); in ZConstp (a, A, instT', inst') end;