1.1 --- a/src/Pure/Syntax/syntax_phases.ML	Thu Jun 27 10:35:37 2013 +0200
     1.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Thu Jun 27 11:07:48 2013 +0200
     1.3 @@ -533,15 +533,16 @@
     1.4      fun aprop t = Syntax.const "_aprop" $ t;
     1.5  
     1.6      fun is_prop Ts t =
     1.7 -      Type_Annotation.fastype_of Ts t = propT handle TERM _ => false;
     1.8 +      Type_Annotation.clean (Type_Annotation.fastype_of Ts t) = propT
     1.9 +        handle TERM _ => false;
    1.10  
    1.11      fun is_term (Const ("Pure.term", _) $ _) = true
    1.12        | is_term _ = false;
    1.13  
    1.14      fun mark _ (t as Const _) = t
    1.15        | mark Ts (t as Const ("_bound", _) $ u) = if is_prop Ts u then aprop t else t
    1.16 -      | mark _ (t as Free (x, T)) = if T = propT then aprop (Syntax.free x) else t
    1.17 -      | mark _ (t as Var (xi, T)) = if T = propT then aprop (Syntax.var xi) else t
    1.18 +      | mark Ts (t as Free _) = if is_prop Ts t then aprop t else t
    1.19 +      | mark Ts (t as Var _) = if is_prop Ts t then aprop t else t
    1.20        | mark Ts (t as Bound _) = if is_prop Ts t then aprop t else t
    1.21        | mark Ts (Abs (x, T, t)) = Abs (x, T, mark (T :: Ts) t)
    1.22        | mark Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =
    1.23 @@ -628,7 +629,12 @@
    1.24        handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
    1.25  
    1.26      and constrain t T0 =
    1.27 -      let val T = Type_Annotation.smash T0 in
    1.28 +      let
    1.29 +        val T =
    1.30 +          if show_markup andalso not show_types
    1.31 +          then Type_Annotation.clean T0
    1.32 +          else Type_Annotation.smash T0;
    1.33 +      in
    1.34          if (show_types orelse show_markup) andalso T <> dummyT then
    1.35            Ast.Appl [Ast.Constant "_constrain", simple_ast_of ctxt t,
    1.36              ast_of_termT ctxt trf (term_of_typ ctxt T)]