src/Pure/General/name_space.ML

 signature NAME_SPACE =
 sig
   type T
   val empty: string -> T
   val kind_of: T -> string
-  val defined_entry: T -> string -> bool
   val the_entry: T -> string ->
     {concealed: bool, group: serial option, theory_name: string, pos: Position.T, serial: serial}
   val entry_ord: T -> string * string -> order
   val markup: T -> string -> Markup.T
   val is_concealed: T -> string -> bool

   val change_ignore: 'a table -> 'a table
   val space_of_table: 'a table -> T
   val check_reports: Context.generic -> 'a table ->
     xstring * Position.T list -> (string * Position.report list) * 'a
   val check: Context.generic -> 'a table -> xstring * Position.T -> string * 'a
+  val defined: 'a table -> string -> bool
   val lookup_key: 'a table -> string -> (string * 'a) option
   val get: 'a table -> string -> 'a
   val define: Context.generic -> bool -> binding * 'a -> 'a table -> string * 'a table
   val alias_table: naming -> binding -> string -> 'a table -> 'a table
   val hide_table: bool -> string -> 'a table -> 'a table

 
 
 fun empty kind = make_name_space (kind, Change_Table.empty, Change_Table.empty);
 
 fun kind_of (Name_Space {kind, ...}) = kind;
-
-fun defined_entry (Name_Space {entries, ...}) = Change_Table.defined entries;
 
 fun the_entry (Name_Space {kind, entries, ...}) name =
   (case Change_Table.lookup entries name of
     NONE => error (undefined kind name)
   | SOME (_, entry) => entry);

   let
     val ((name, reports), x) = check_reports context table (xname, [pos]);
     val _ = Position.reports reports;
   in (name, x) end;
 
+fun defined (Table (_, tab)) name = Change_Table.defined tab name;
 fun lookup_key (Table (_, tab)) name = Change_Table.lookup_key tab name;
 
 fun get table name =
   (case lookup_key table name of
     SOME (_, x) => x