proper support for complex types, not just type variables (amending 623789141e39);

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