--- a/src/Pure/General/name_space.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/General/name_space.ML Sun Nov 25 19:49:24 2012 +0100
@@ -88,7 +88,7 @@
id: serial};
fun entry_markup def kind (name, {pos, id, ...}: entry) =
- Markup.properties (Position.entity_properties_of def id pos) (Isabelle_Markup.entity kind name);
+ Markup.properties (Position.entity_properties_of def id pos) (Markup.entity kind name);
fun print_entry_ref kind (name, entry) =
quote (Markup.markup (entry_markup false kind (name, entry)) name);
@@ -133,7 +133,7 @@
fun markup (Name_Space {kind, entries, ...}) name =
(case Symtab.lookup entries name of
- NONE => Isabelle_Markup.intensify
+ NONE => Markup.intensify
| SOME (_, entry) => entry_markup false kind (name, entry));
fun is_concealed space name = #concealed (the_entry space name);