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