# HG changeset patch
# User wenzelm
# Date 1427825257 -7200
# Node ID 12a89103cae65033ca8db4120db6768c8019bf60
# Parent  ada832308efe39699fff7695ebea920cd691a4ec
tuned signature;

diff -r ada832308efe -r 12a89103cae6 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Tue Mar 31 19:39:05 2015 +0200
+++ b/src/Pure/General/name_space.ML	Tue Mar 31 20:07:37 2015 +0200
@@ -12,7 +12,6 @@
   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
@@ -62,6 +61,7 @@
   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
@@ -147,8 +147,6 @@
 
 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)
@@ -497,6 +495,7 @@
     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 =
diff -r ada832308efe -r 12a89103cae6 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Tue Mar 31 19:39:05 2015 +0200
+++ b/src/Pure/facts.ML	Tue Mar 31 20:07:37 2015 +0200
@@ -166,7 +166,7 @@
 
 (* retrieve *)
 
-val defined = is_some oo (Name_Space.lookup_key o facts_of);
+val defined = Name_Space.defined o facts_of;
 
 fun lookup context facts name =
   (case Name_Space.lookup_key (facts_of facts) name of
diff -r ada832308efe -r 12a89103cae6 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Tue Mar 31 19:39:05 2015 +0200
+++ b/src/Pure/variable.ML	Tue Mar 31 20:07:37 2015 +0200
@@ -347,7 +347,7 @@
 
 (* specialized name space *)
 
-val is_fixed = Name_Space.defined_entry o fixes_space;
+val is_fixed = Name_Space.defined o fixes_of;
 fun is_newly_fixed inner outer = is_fixed inner andf (not o is_fixed outer);
 
 val fixed_ord = Name_Space.entry_ord o fixes_space;