--- a/src/Pure/Isar/proof_context.ML Wed Mar 30 22:45:10 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML Wed Mar 30 22:53:18 2011 +0200
@@ -673,7 +673,7 @@
markup_const = fn x => [Name_Space.markup_entry (const_space ctxt) x],
markup_free = fn x =>
[if can Name.dest_skolem x then Markup.skolem else Markup.free] @
- (if Variable.is_fixed ctxt x then [] else [Markup.hilite]),
+ (if not (Variable.is_body ctxt) orelse Variable.is_fixed ctxt x then [] else [Markup.hilite]),
markup_var = fn xi => [Markup.name (Term.string_of_vname xi) Markup.var]};
val decode_term = Syntax.decode_term o term_context;