src/Pure/logic.ML

--- a/src/Pure/logic.ML	Fri Nov 29 11:26:17 2024 +0100
+++ b/src/Pure/logic.ML	Fri Nov 29 17:40:15 2024 +0100
@@ -335,7 +335,7 @@
 fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c]));
 
 fun mk_arities (t, Ss, S) =
-  let val T = Type (t, ListPair.map TFree (Name.invent Name.context Name.aT (length Ss), Ss))
+  let val T = Type (t, ListPair.map TFree (Name.invent_global_types (length Ss), Ss))
   in map (fn c => mk_of_class (T, c)) S end;
 
 fun mk_arity (t, Ss, c) = the_single (mk_arities (t, Ss, [c]));
@@ -375,7 +375,7 @@
     val {present, extra} = present_sorts shyps present_set;
 
     val n = Types.size present_set;
-    val (names1, names2) = Name.invent Name.context Name.aT (n + length extra) |> chop n;
+    val (names1, names2) = Name.invent_global_types (n + length extra) |> chop n;
 
     val present_map =
       map2 (fn (T, S) => fn a => (T, TVar ((a, 0), S))) present names1;