# HG changeset patch
# User wenzelm
# Date 1724417793 -7200
# Node ID 515a6659cb7bf9af80a37d5d741ecb478fdaefd5
# Parent  94e64d8ac668be03565466f8fcb04964de6d37c9
clarified markup: more uniform;

diff -r 94e64d8ac668 -r 515a6659cb7b src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Aug 23 14:41:45 2024 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri Aug 23 14:56:33 2024 +0200
@@ -570,8 +570,7 @@
           let
             val reports = ps
               |> filter (Context_Position.is_reported ctxt)
-              |> map (fn pos =>
-                (pos, Markup.name x (if Name.is_skolem x then Markup.skolem else Markup.free)));
+              |> map (fn pos => (pos, Markup.name x (Variable.markup ctxt x)));
           in (Free (x, infer_type ctxt (x, dummyT)), reports) end
       | (_, SOME d) =>
           let
diff -r 94e64d8ac668 -r 515a6659cb7b src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Fri Aug 23 14:41:45 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Aug 23 14:56:33 2024 +0200
@@ -708,7 +708,7 @@
     val m1 =
       if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt
       then Markup.fixed x else Markup.intensify;
-    val m2 = if Name.is_skolem x then Markup.skolem else Markup.free;
+    val m2 = Variable.markup ctxt x;
   in [m1, m2] end;
 
 fun markup ctxt c =