--- a/src/Pure/thm.ML Mon Apr 10 18:08:23 2023 +0200
+++ b/src/Pure/thm.ML Mon Apr 10 18:13:23 2023 +0200
@@ -1640,7 +1640,7 @@
val add_instT_sorts = add_sorts (fn Ctyp {sorts, ...} => sorts);
val add_inst_sorts = add_sorts (fn Cterm {sorts, ...} => sorts);
-fun make_instT thy (v as (_, S)) (Ctyp {T = U, maxidx, ...}) =
+fun make_instT thy (_: indexname, S) (Ctyp {T = U, maxidx, ...}) =
if Sign.of_sort thy (U, S) then (U, maxidx)
else raise TYPE ("Type not of sort " ^ Syntax.string_of_sort_global thy S, [U], []);