# HG changeset patch
# User wenzelm
# Date 1732969903 -3600
# Node ID 08d492f6c1b5dc9b14a67dd653bddda6da23637c
# Parent  1052f79afe217f859bb70ce1c1f1f8cee07a3ac3
tuned signature: more operations;

diff -r 1052f79afe21 -r 08d492f6c1b5 src/Pure/name.ML
--- a/src/Pure/name.ML	Sat Nov 30 12:30:18 2024 +0100
+++ b/src/Pure/name.ML	Sat Nov 30 13:31:43 2024 +0100
@@ -33,6 +33,7 @@
   val invent_global_types: int -> string list
   val invent_names: context -> string -> 'a list -> (string * 'a) list
   val invent_names_global: string -> 'a list -> (string * 'a) list
+  val invent_types: context -> 'a list -> (string * 'a) list
   val invent_types_global: 'a list -> (string * 'a) list
   val invent_list: string list -> string -> int -> string list
   val variant: string -> context -> string * context
@@ -135,7 +136,9 @@
 
 fun invent_names ctxt x xs = invent ctxt x (length xs) ~~ xs;
 fun invent_names_global x xs = invent_names context x xs;
-fun invent_types_global xs = invent_names context aT xs;
+
+fun invent_types ctxt xs = invent_names ctxt aT xs;
+fun invent_types_global xs = invent_types context xs;
 
 val invent_list = invent o make_context;