1.1 --- a/src/HOL/Groups.thy	Tue May 28 13:14:31 2013 +0200
     1.2 +++ b/src/HOL/Groups.thy	Tue May 28 16:29:11 2013 +0200
     1.3 @@ -124,12 +124,10 @@
     1.4  typed_print_translation {*
     1.5    let
     1.6      fun tr' c = (c, fn ctxt => fn T => fn ts =>
     1.7 -      if not (null ts) orelse T = dummyT orelse
     1.8 -        not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T
     1.9 -      then raise Match
    1.10 -      else
    1.11 +      if null ts andalso Printer.type_emphasis ctxt T then
    1.12          Syntax.const @{syntax_const "_constrain"} $ Syntax.const c $
    1.13 -          Syntax_Phases.term_of_typ ctxt T);
    1.14 +          Syntax_Phases.term_of_typ ctxt T
    1.15 +      else raise Match);
    1.16    in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
    1.17  *} -- {* show types that are presumably too general *}
    1.18  

     2.1 --- a/src/HOL/Num.thy	Tue May 28 13:14:31 2013 +0200
     2.2 +++ b/src/HOL/Num.thy	Tue May 28 16:29:11 2013 +0200
     2.3 @@ -332,8 +332,10 @@
     2.4        in
     2.5          (case T of
     2.6            Type (@{type_name fun}, [_, T']) =>
     2.7 -            if not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T' then t'
     2.8 -            else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T'
     2.9 +            if Printer.type_emphasis ctxt T' then
    2.10 +              Syntax.const @{syntax_const "_constrain"} $ t' $
    2.11 +                Syntax_Phases.term_of_typ ctxt T'
    2.12 +            else t'
    2.13          | _ => if T = dummyT then t' else raise Match)
    2.14        end;
    2.15    in

     3.1 --- a/src/HOL/ex/Numeral_Representation.thy	Tue May 28 13:14:31 2013 +0200
     3.2 +++ b/src/HOL/ex/Numeral_Representation.thy	Tue May 28 16:29:11 2013 +0200
     3.3 @@ -306,11 +306,13 @@
     3.4          val k = int_of_num' n;
     3.5          val t' = Syntax.const @{syntax_const "_Numerals"} $ Syntax.free ("#" ^ string_of_int k);
     3.6        in
     3.7 -        case T of
     3.8 +        (case T of
     3.9            Type (@{type_name fun}, [_, T']) =>
    3.10 -            if not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T' then t'
    3.11 -            else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T'
    3.12 -        | T' => if T' = dummyT then t' else raise Match
    3.13 +            if Printer.type_emphasis ctxt T' then
    3.14 +              Syntax.const @{syntax_const "_constrain"} $ t' $
    3.15 +                Syntax_Phases.term_of_typ ctxt T'
    3.16 +            else t'
    3.17 +        | T' => if T' = dummyT then t' else raise Match)
    3.18        end;
    3.19    in [(@{const_syntax of_num}, num_tr')] end
    3.20  *}

     4.1 --- a/src/Pure/Syntax/printer.ML	Tue May 28 13:14:31 2013 +0200
     4.2 +++ b/src/Pure/Syntax/printer.ML	Tue May 28 16:29:11 2013 +0200
     4.3 @@ -26,8 +26,8 @@
     4.4    val show_markup_raw: Config.raw
     4.5    val show_structs_raw: Config.raw
     4.6    val show_question_marks_raw: Config.raw
     4.7 -  val show_type_constraint: Proof.context -> bool
     4.8 -  val show_sort_constraint: Proof.context -> bool
     4.9 +  val show_type_emphasis: bool Config.T
    4.10 +  val type_emphasis: Proof.context -> typ -> bool
    4.11    type prtabs
    4.12    val empty_prtabs: prtabs
    4.13    val update_prtabs: string -> Syntax_Ext.xprod list -> prtabs -> prtabs
    4.14 @@ -70,8 +70,13 @@
    4.15  val show_question_marks_raw = Config.declare_option "show_question_marks";
    4.16  val show_question_marks = Config.bool show_question_marks_raw;
    4.17  
    4.18 -fun show_type_constraint ctxt = Config.get ctxt show_types orelse Config.get ctxt show_markup;
    4.19 -fun show_sort_constraint ctxt = Config.get ctxt show_sorts orelse Config.get ctxt show_markup;
    4.20 +val show_type_emphasis =
    4.21 +  Config.bool (Config.declare "show_type_emphasis" (fn _ => Config.Bool true));
    4.22 +
    4.23 +fun type_emphasis ctxt T =
    4.24 +  T <> dummyT andalso
    4.25 +    (Config.get ctxt show_types orelse Config.get ctxt show_markup orelse
    4.26 +      Config.get ctxt show_type_emphasis andalso not (can dest_Type T));
    4.27  
    4.28  
    4.29  

     5.1 --- a/src/Pure/Syntax/syntax_phases.ML	Tue May 28 13:14:31 2013 +0200
     5.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Tue May 28 16:29:11 2013 +0200
     5.3 @@ -470,10 +470,10 @@
     5.4  
     5.5  fun term_of_typ ctxt ty =
     5.6    let
     5.7 -    val show_sort_constraint = Printer.show_sort_constraint ctxt;
     5.8 +    val show_sorts = Config.get ctxt show_sorts orelse Config.get ctxt show_markup;
     5.9  
    5.10      fun ofsort t raw_S =
    5.11 -      if show_sort_constraint then
    5.12 +      if show_sorts then
    5.13          let val S = #2 (Term_Position.decode_positionS raw_S)
    5.14          in if S = dummyS then t else Syntax.const "_ofsort" $ t $ term_of_sort S end
    5.15        else t;