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

diff -r 12a89103cae6 -r bbf49d7dfd6f src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Tue Mar 31 20:07:37 2015 +0200
+++ b/src/Pure/General/name_space.ML	Tue Mar 31 20:18:10 2015 +0200
@@ -62,6 +62,7 @@
     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: 'a table -> string -> 'a option
   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
@@ -162,9 +163,9 @@
 fun is_concealed space name = #concealed (the_entry space name);
 
 
-(* name accesses *)
+(* intern *)
 
-fun lookup (Name_Space {internals, ...}) xname =
+fun intern' (Name_Space {internals, ...}) xname =
   (case Change_Table.lookup internals xname of
     NONE => (xname, true)
   | SOME ([], []) => (xname, true)
@@ -172,6 +173,8 @@
   | SOME (name :: _, _) => (name, false)
   | SOME ([], name' :: _) => (Long_Name.hidden name', true));
 
+val intern = #1 oo intern';
+
 fun get_accesses (Name_Space {entries, ...}) name =
   (case Change_Table.lookup entries name of
     NONE => [name]
@@ -182,11 +185,6 @@
     if not (null names) andalso hd names = name then cons xname else I) internals [];
 
 
-(* intern *)
-
-fun intern space xname = #1 (lookup space xname);
-
-
 (* extern *)
 
 val names_long_raw = Config.declare_option ("names_long", @{here});
@@ -205,7 +203,7 @@
     val names_unique = Config.get ctxt names_unique;
 
     fun valid require_unique xname =
-      let val (name', is_unique) = lookup space xname
+      let val (name', is_unique) = intern' space xname
       in name = name' andalso (not require_unique orelse is_unique) end;
 
     fun ext [] = if valid false name then name else Long_Name.hidden name
@@ -496,6 +494,7 @@
   in (name, x) end;
 
 fun defined (Table (_, tab)) name = Change_Table.defined tab name;
+fun lookup (Table (_, tab)) name = Change_Table.lookup tab name;
 fun lookup_key (Table (_, tab)) name = Change_Table.lookup_key tab name;
 
 fun get table name =
diff -r 12a89103cae6 -r bbf49d7dfd6f src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Mar 31 20:07:37 2015 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Mar 31 20:18:10 2015 +0200
@@ -180,7 +180,7 @@
 fun markup_name ctxt name = markup_extern ctxt name |-> Markup.markup;
 fun pretty_name ctxt name = markup_extern ctxt name |> Pretty.mark_str;
 
-val get_locale = Option.map #2 oo (Name_Space.lookup_key o Locales.get);
+val get_locale = Name_Space.lookup o Locales.get;
 val defined = is_some oo get_locale;
 
 fun the_locale thy name =
diff -r 12a89103cae6 -r bbf49d7dfd6f src/Pure/facts.ML
--- a/src/Pure/facts.ML	Tue Mar 31 20:07:37 2015 +0200
+++ b/src/Pure/facts.ML	Tue Mar 31 20:18:10 2015 +0200
@@ -169,10 +169,10 @@
 val defined = Name_Space.defined o facts_of;
 
 fun lookup context facts name =
-  (case Name_Space.lookup_key (facts_of facts) name of
+  (case Name_Space.lookup (facts_of facts) name of
     NONE => NONE
-  | SOME (_, Static ths) => SOME (true, ths)
-  | SOME (_, Dynamic f) => SOME (false, f context));
+  | SOME (Static ths) => SOME (true, ths)
+  | SOME (Dynamic f) => SOME (false, f context));
 
 fun retrieve context facts (xname, pos) =
   let
diff -r 12a89103cae6 -r bbf49d7dfd6f src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Mar 31 20:07:37 2015 +0200
+++ b/src/Pure/thm.ML	Tue Mar 31 20:18:10 2015 +0200
@@ -590,8 +590,8 @@
 fun axiom theory name =
   let
     fun get_ax thy =
-      Name_Space.lookup_key (Theory.axiom_table thy) name
-      |> Option.map (fn (_, prop) =>
+      Name_Space.lookup (Theory.axiom_table thy) name
+      |> Option.map (fn prop =>
            let
              val der = deriv_rule0 (Proofterm.axm_proof name prop);
              val maxidx = maxidx_of_term prop;
diff -r 12a89103cae6 -r bbf49d7dfd6f src/Pure/type.ML
--- a/src/Pure/type.ML	Tue Mar 31 20:07:37 2015 +0200
+++ b/src/Pure/type.ML	Tue Mar 31 20:18:10 2015 +0200
@@ -254,7 +254,7 @@
 
 fun undecl_type c = "Undeclared type constructor: " ^ quote c;
 
-fun lookup_type (TSig {types, ...}) = Option.map #2 o Name_Space.lookup_key types;
+fun lookup_type (TSig {types, ...}) = Name_Space.lookup types;
 
 fun check_decl context (TSig {types, ...}) (c, pos) =
   Name_Space.check_reports context types (c, [pos]);
diff -r 12a89103cae6 -r bbf49d7dfd6f src/Pure/variable.ML
--- a/src/Pure/variable.ML	Tue Mar 31 20:07:37 2015 +0200
+++ b/src/Pure/variable.ML	Tue Mar 31 20:18:10 2015 +0200
@@ -340,8 +340,8 @@
 fun restore_proper_fixes ctxt = Config.put proper_fixes (Config.get ctxt proper_fixes);
 
 fun is_improper ctxt x =
-  (case Name_Space.lookup_key (fixes_of ctxt) x of
-    SOME (_, (_, proper)) => not proper
+  (case Name_Space.lookup (fixes_of ctxt) x of
+    SOME (_, proper) => not proper
   | NONE => false);
 
 
@@ -358,8 +358,8 @@
   in if is_fixed ctxt x' then SOME x' else NONE end;
 
 fun revert_fixed ctxt x =
-  (case Name_Space.lookup_key (fixes_of ctxt) x of
-    SOME (_, (x', _)) => if intern_fixed ctxt x' = x then x' else x
+  (case Name_Space.lookup (fixes_of ctxt) x of
+    SOME (x', _) => if intern_fixed ctxt x' = x then x' else x
   | NONE => x);
 
 fun markup_fixed ctxt x =