# HG changeset patch
# User wenzelm
# Date 1729966731 -7200
# Node ID 2daa7b2ef46e7429654446bb967e461b4e35467a
# Parent  6eccae3387706b101eab124edeed4aea0fc6785c
clarified (again): Markup.intensify is already part of Variable.markup_fixed for undeclared variable, Markup.fixed is already part of Mariable.markup;

diff -r 6eccae338770 -r 2daa7b2ef46e src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Sat Oct 26 16:07:31 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Sat Oct 26 20:18:51 2024 +0200
@@ -54,12 +54,10 @@
 
 fun markup_free ctxt x =
   let
-    val m1 =
-      if Variable.is_fixed ctxt x then Variable.markup_fixed ctxt x
-      else if not (Variable.is_body ctxt) orelse Syntax.is_pretty_global ctxt then Markup.fixed x
-      else Markup.intensify;
+    val strict = Variable.is_body ctxt andalso not (Syntax.is_pretty_global ctxt);
+    val m1 = if Variable.is_fixed ctxt x orelse strict then [Variable.markup_fixed ctxt x] else [];
     val m2 = Variable.markup ctxt x;
-  in [m1, m2] end;
+  in m1 @ [m2] end;
 
 fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var];