src/HOL/Groups.thy
changeset 52210 0226035df99d
parent 52143 36ffe23b25f8
child 52289 83ce5d2841e7
     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