src/Pure/sign.ML

   let
     val thy = Proof_Context.theory_of ctxt;
     fun print_type c = uncurry Markup.markup (Name_Space.markup_extern ctxt (type_space thy) c);
     fun print_const c = uncurry Markup.markup (Name_Space.markup_extern ctxt (const_space thy) c);
   in
-    s |> Lexicon.unmark
+    s |> Lexicon.unmark_entity
      {case_class = K (),
       case_type = fn c =>
         if declared_tyname thy c then () else error ("Not a global type: " ^ quote (print_type c)),
       case_const = fn c =>
         if declared_const thy c then () else error ("Not a global const: " ^ quote (print_const c)),