diff -r 9d2fae6b31cc -r dc8a8a7559e7 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Thu Apr 14 22:55:53 2016 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Apr 14 23:31:10 2016 +0200
@@ -51,9 +51,7 @@
   [Name_Space.markup (Consts.space_of (Proof_Context.consts_of ctxt)) c];
 
 fun markup_free ctxt x =
-  (if Variable.is_improper ctxt x then Markup.improper
-   else if Name.is_skolem x then Markup.skolem
-   else Markup.free) ::
+  Variable.markup ctxt x ::
   (if Variable.is_body ctxt orelse Variable.is_fixed ctxt x
    then [Variable.markup_fixed ctxt x]
    else []);