# HG changeset patch
# User wenzelm
# Date 1211027222 -7200
# Node ID 64e50d7832768a51aea38e06979c3e4f62b56903
# Parent  bad4e1819b42713d4d11d836ab75e475f0202c47
default token translations: observe Sign.is_pretty_global for fixed variables;

diff -r bad4e1819b42 -r 64e50d783276 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat May 17 14:27:01 2008 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat May 17 14:27:02 2008 +0200
@@ -364,7 +364,9 @@
 fun free_or_skolem ctxt x =
   (if can Name.dest_skolem x then Pretty.mark Markup.skolem (Pretty.str (revert_skolem ctxt x))
    else Pretty.mark Markup.free (Pretty.str x))
-  |> Pretty.mark (if Variable.is_fixed ctxt x then Markup.fixed x else Markup.hilite);
+  |> Pretty.mark
+    (if Variable.is_fixed ctxt x orelse Sign.is_pretty_global ctxt then Markup.fixed x
+     else Markup.hilite);
 
 fun var_or_skolem _ s =
   (case Lexicon.read_variable s of