# HG changeset patch
# User wenzelm
# Date 1704233863 -3600
# Node ID a4eae462f224df2e168870929d5e160416994ce8
# Parent  623789141e398598915309d5aaef835e1609f7be
proper support for complex types, not just type variables (amending 623789141e39);

diff -r 623789141e39 -r a4eae462f224 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Tue Jan 02 21:58:32 2024 +0100
+++ b/src/Pure/zterm.ML	Tue Jan 02 23:17:43 2024 +0100
@@ -787,7 +787,7 @@
 
 fun make_const_proof (f, g) (a, A, instT, inst) =
   let
-    val typ = Same.function (fn ZTVar ((x, _), _) => try f x | _ => NONE);
+    val typ = subst_type_same (Same.function (fn ((x, _), _) => try f x));
     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;