src/Pure/theory.ML
changeset 81507 08574da77b4a
parent 80074 951c371c1cd9
--- a/src/Pure/theory.ML	Fri Nov 29 11:26:17 2024 +0100
+++ b/src/Pure/theory.ML	Fri Nov 29 17:40:15 2024 +0100
@@ -287,7 +287,7 @@
 fun add_deps_type c thy =
   let
     val n = Sign.arity_number thy c;
-    val args = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT n);
+    val args = map (fn a => TFree (a, [])) (Name.invent_global_types n);
   in thy |> add_deps_global "" (type_dep (c, args)) [] end
 
 fun specify_const decl thy =