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 =