src/Pure/General/name_space.ML

--- a/src/Pure/General/name_space.ML	Tue Sep 07 21:16:22 2021 +0200
+++ b/src/Pure/General/name_space.ML	Tue Sep 07 21:47:50 2021 +0200
@@ -117,7 +117,7 @@
   Position.make_entity_markup def serial kind (name, pos);
 
 fun print_entry_ref kind (name, entry) =
-  quote (Markup.markup (entry_markup false kind (name, entry)) name);
+  quote (Markup.markup (entry_markup {def = false} kind (name, entry)) name);
 
 fun err_dup kind entry1 entry2 pos =
   error ("Duplicate " ^ plain_words kind ^ " declaration " ^
@@ -170,8 +170,8 @@
     NONE => Markup.intensify
   | SOME (_, entry) => entry_markup def kind (name, entry));
 
-val markup = gen_markup false;
-val markup_def = gen_markup true;
+val markup = gen_markup {def = false};
+val markup_def = gen_markup {def = true};
 
 fun undefined (space as Name_Space {kind, entries, ...}) bad =
   let
@@ -545,7 +545,7 @@
         in (kind, internals', entries') end);
     val _ =
       if proper_pos andalso Context_Position.is_reported_generic context pos then
-        Position.report pos (entry_markup true (kind_of space) (name, entry))
+        Position.report pos (entry_markup {def = true} (kind_of space) (name, entry))
       else ();
   in (name, space') end;