# HG changeset patch
# User wenzelm
# Date 1301518398 -7200
# Node ID 5d33c12ccf2292c9c18bb26e3759289707200568
# Parent  e86b10c68f0b1872c02983a23cf1117523c5d7f2
accomodate autofix discipline of non-body context;

diff -r e86b10c68f0b -r 5d33c12ccf22 src/Pure/Isar/proof_context.ML
--- 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;