default token translations: observe Sign.is_pretty_global for fixed variables;

--- 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