Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
proper instantiation for make_const_proof, notably change of types for term variables;
authorwenzelm
Tue, 02 Jan 2024 21:58:32 +0100
changeset 79416 623789141e39
parent 79415 740ec03b0b71
child 79417 a4eae462f224
proper instantiation for make_const_proof, notably change of types for term variables;
src/Pure/zterm.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle