1.1 --- a/src/Pure/Syntax/syntax_phases.ML	Sat Sep 29 16:51:04 2012 +0200
     1.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Sat Sep 29 18:23:46 2012 +0200
     1.3 @@ -550,8 +550,12 @@
     1.4            Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts)
     1.5        | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
     1.6            Ast.mk_appl (constrain (c $ Syntax.var xi) T) (map ast_of ts)
     1.7 -      | ((c as Const ("_bound", _)), Free (x, T) :: ts) =>
     1.8 -          Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts)
     1.9 +      | ((c as Const ("_bound", B)), Free (x, T) :: ts) =>
    1.10 +          let
    1.11 +            val X =
    1.12 +              if show_markup andalso not show_types orelse B <> dummyT then T
    1.13 +              else dummyT;
    1.14 +          in Ast.mk_appl (constrain (c $ Syntax.free x) X) (map ast_of ts) end
    1.15        | (Const ("_idtdummy", T), ts) =>
    1.16            Ast.mk_appl (constrain (Syntax.const "_idtdummy") T) (map ast_of ts)
    1.17        | (const as Const (c, T), ts) =>