# HG changeset patch
# User wenzelm
# Date 1681143203 -7200
# Node ID 849c996f052b2aa0a34514fac5f0519e1f3c67d3
# Parent  f34d11942ac12159b967323836f20c5180c5681e
tuned;

diff -r f34d11942ac1 -r 849c996f052b src/Pure/thm.ML
--- 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], []);