src/HOL/Num.thy
changeset 52210 0226035df99d
parent 52187 1f7b3aadec69
child 52435 6646bb548c6b
     1.1 --- a/src/HOL/Num.thy	Tue May 28 13:14:31 2013 +0200
     1.2 +++ b/src/HOL/Num.thy	Tue May 28 16:29:11 2013 +0200
     1.3 @@ -332,8 +332,10 @@
     1.4        in
     1.5          (case T of
     1.6            Type (@{type_name fun}, [_, T']) =>
     1.7 -            if not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T' then t'
     1.8 -            else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T'
     1.9 +            if Printer.type_emphasis ctxt T' then
    1.10 +              Syntax.const @{syntax_const "_constrain"} $ t' $
    1.11 +                Syntax_Phases.term_of_typ ctxt T'
    1.12 +            else t'
    1.13          | _ => if T = dummyT then t' else raise Match)
    1.14        end;
    1.15    in