diff -r 56075edacb10 -r bf19ea589f99 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Sun Dec 08 19:05:05 2024 +0100 +++ b/src/Pure/Syntax/syntax_phases.ML Sun Dec 08 20:09:14 2024 +0100 @@ -44,13 +44,13 @@ (** markup logical entities **) fun markup_class ctxt c = - [Name_Space.markup (Type.class_space (Proof_Context.tsig_of ctxt)) c]; + [Name_Space.markup (Type.class_space (Proof_Context.tsig_of ctxt)) c, Markup.tclass]; fun markup_type ctxt c = - [Name_Space.markup (Type.type_space (Proof_Context.tsig_of ctxt)) c]; + [Name_Space.markup (Type.type_space (Proof_Context.tsig_of ctxt)) c, Markup.tconst]; fun markup_const ctxt c = - [Name_Space.markup (Consts.space_of (Proof_Context.consts_of ctxt)) c]; + [Name_Space.markup (Consts.space_of (Proof_Context.consts_of ctxt)) c, Markup.const]; fun markup_free ctxt x = let