diff -r 4bc55652c685 -r da200fa2768c src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Sun Mar 27 19:51:51 2011 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Sun Mar 27 20:55:01 2011 +0200
@@ -129,20 +129,20 @@
 
 (* decode_term -- transform parse tree into raw term *)
 
-val markup_const = Markup.const;
-fun markup_free x = Markup.name x Markup.free;
-fun markup_var xi = Markup.name (Term.string_of_vname xi) Markup.var;
-
 fun markup_bound def id =
   Markup.properties [(if def then Markup.defN else Markup.refN, id)] Markup.bound;
 
 type term_context =
  {get_sort: (indexname * sort) list -> indexname -> sort,
   get_const: string -> bool * string,
-  get_free: string -> string option};
+  get_free: string -> string option,
+  markup_const: string -> Markup.T,
+  markup_free: string -> Markup.T,
+  markup_var: indexname -> Markup.T};
 
-fun decode_term ({get_sort, get_const, get_free}: term_context) tm =
+fun decode_term (term_context: term_context) tm =
   let
+    val {get_sort, get_const, get_free, markup_const, markup_free, markup_var} = term_context;
     val decodeT = typ_of_term (get_sort (term_sorts tm));
 
     val reports = Unsynchronized.ref ([]: (Position.T * Markup.T) list);