src/Pure/Syntax/syntax_phases.ML
changeset 81565 bf19ea589f99
parent 81558 b57996a0688c
child 81572 693a95492008
--- 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