tuned signature;

--- a/src/Pure/General/name_space.ML	Sun Apr 17 20:58:43 2011 +0200
+++ b/src/Pure/General/name_space.ML	Sun Apr 17 21:04:22 2011 +0200
@@ -16,7 +16,7 @@
   val kind_of: T -> string
   val the_entry: T -> string ->
     {concealed: bool, group: serial option, theory_name: string, pos: Position.T, id: serial}
-  val markup_entry: T -> string -> Markup.T
+  val markup: T -> string -> Markup.T
   val is_concealed: T -> string -> bool
   val intern: T -> xstring -> string
   val long_names_default: bool Unsynchronized.ref
@@ -121,7 +121,7 @@
     NONE => error ("Unknown " ^ kind ^ " " ^ quote name)
   | SOME (_, entry) => entry);
 
-fun markup_entry (Name_Space {kind, entries, ...}) name =
+fun markup (Name_Space {kind, entries, ...}) name =
   (case Symtab.lookup entries name of
     NONE => Markup.malformed
   | SOME (_, entry) => entry_markup false kind (name, entry));

--- a/src/Pure/Isar/proof_context.ML	Sun Apr 17 20:58:43 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Apr 17 21:04:22 2011 +0200
@@ -333,7 +333,7 @@
     then local_facts else global_facts
   end;
 
-fun markup_fact ctxt name = Name_Space.markup_entry (Facts.space_of (which_facts ctxt name)) name;
+fun markup_fact ctxt name = Name_Space.markup (Facts.space_of (which_facts ctxt name)) name;
 
 fun extern_fact ctxt name = Facts.extern ctxt (which_facts ctxt name) name;
 
@@ -888,7 +888,7 @@
             (case Facts.lookup (Context.Proof ctxt) local_facts name of
               SOME (_, ths) =>
                 (Context_Position.report ctxt pos
-                  (Name_Space.markup_entry (Facts.space_of local_facts) name);
+                  (Name_Space.markup (Facts.space_of local_facts) name);
                  map (Thm.transfer thy) (Facts.select thmref ths))
             | NONE => Global_Theory.get_fact (Context.Proof ctxt) thy xthmref);
       in pick name thms end;

--- a/src/Pure/Syntax/syntax_phases.ML	Sun Apr 17 20:58:43 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Sun Apr 17 21:04:22 2011 +0200
@@ -21,13 +21,13 @@
 (** markup logical entities **)
 
 fun markup_class ctxt c =
-  [Name_Space.markup_entry (Type.class_space (Proof_Context.tsig_of ctxt)) c];
+  [Name_Space.markup (Type.class_space (Proof_Context.tsig_of ctxt)) c];
 
 fun markup_type ctxt c =
-  [Name_Space.markup_entry (Type.type_space (Proof_Context.tsig_of ctxt)) c];
+  [Name_Space.markup (Type.type_space (Proof_Context.tsig_of ctxt)) c];
 
 fun markup_const ctxt c =
-  [Name_Space.markup_entry (Consts.space_of (Proof_Context.consts_of ctxt)) c];
+  [Name_Space.markup (Consts.space_of (Proof_Context.consts_of ctxt)) c];
 
 fun markup_free ctxt x =
   [if can Name.dest_skolem x then Markup.skolem else Markup.free] @

--- a/src/Pure/global_theory.ML	Sun Apr 17 20:58:43 2011 +0200
+++ b/src/Pure/global_theory.ML	Sun Apr 17 21:04:22 2011 +0200
@@ -91,7 +91,7 @@
     (case res of
       NONE => error ("Unknown fact " ^ quote name ^ Position.str_of pos)
     | SOME (static, ths) =>
-        (Context_Position.report ctxt pos (Name_Space.markup_entry (Facts.space_of facts) name);
+        (Context_Position.report ctxt pos (Name_Space.markup (Facts.space_of facts) name);
          if static then () else Context_Position.report ctxt pos (Markup.dynamic_fact name);
          Facts.select xthmref (map (Thm.transfer thy) ths)))
   end;