src/Pure/Isar/proof_context.ML
changeset 26930 64e50d783276
parent 26731 48df747c8543
child 26939 1035c89b4c02
     1.1 --- a/src/Pure/Isar/proof_context.ML	Sat May 17 14:27:01 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Sat May 17 14:27:02 2008 +0200
     1.3 @@ -364,7 +364,9 @@
     1.4  fun free_or_skolem ctxt x =
     1.5    (if can Name.dest_skolem x then Pretty.mark Markup.skolem (Pretty.str (revert_skolem ctxt x))
     1.6     else Pretty.mark Markup.free (Pretty.str x))
     1.7 -  |> Pretty.mark (if Variable.is_fixed ctxt x then Markup.fixed x else Markup.hilite);
     1.8 +  |> Pretty.mark
     1.9 +    (if Variable.is_fixed ctxt x orelse Sign.is_pretty_global ctxt then Markup.fixed x
    1.10 +     else Markup.hilite);
    1.11  
    1.12  fun var_or_skolem _ s =
    1.13    (case Lexicon.read_variable s of