src/HOL/Groups.thy
changeset 49690 a6814de45b69
parent 49388 1ffd5a055acf
child 51546 2e26df807dc7
     1.1 --- a/src/HOL/Groups.thy	Wed Oct 03 16:59:20 2012 +0200
     1.2 +++ b/src/HOL/Groups.thy	Wed Oct 03 16:59:58 2012 +0200
     1.3 @@ -124,8 +124,8 @@
     1.4  typed_print_translation (advanced) {*
     1.5    let
     1.6      fun tr' c = (c, fn ctxt => fn T => fn ts =>
     1.7 -      if not (null ts) orelse T = dummyT
     1.8 -        orelse not (Config.get ctxt show_types) andalso can Term.dest_Type T
     1.9 +      if not (null ts) orelse T = dummyT orelse
    1.10 +        not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T
    1.11        then raise Match
    1.12        else
    1.13          Syntax.const @{syntax_const "_constrain"} $ Syntax.const c $