--- a/src/HOL/Groups.thy Wed Oct 03 16:59:20 2012 +0200
+++ b/src/HOL/Groups.thy Wed Oct 03 16:59:58 2012 +0200
@@ -124,8 +124,8 @@
typed_print_translation (advanced) {*
let
fun tr' c = (c, fn ctxt => fn T => fn ts =>
- if not (null ts) orelse T = dummyT
- orelse not (Config.get ctxt show_types) andalso can Term.dest_Type T
+ if not (null ts) orelse T = dummyT orelse
+ not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T
then raise Match
else
Syntax.const @{syntax_const "_constrain"} $ Syntax.const c $