src/HOL/Groups.thy
changeset 39134 917b4b6ba3d2
parent 37986 3b3187adf292
child 40368 47c186c8577d
     1.1 --- a/src/HOL/Groups.thy	Sun Sep 05 19:47:40 2010 +0200
     1.2 +++ b/src/HOL/Groups.thy	Sun Sep 05 21:41:24 2010 +0200
     1.3 @@ -124,11 +124,11 @@
     1.4  simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
     1.5  simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
     1.6  
     1.7 -typed_print_translation {*
     1.8 +typed_print_translation (advanced) {*
     1.9  let
    1.10 -  fun tr' c = (c, fn show_sorts => fn T => fn ts =>
    1.11 -    if (not o null) ts orelse T = dummyT
    1.12 -      orelse not (! show_types) andalso can Term.dest_Type T
    1.13 +  fun tr' c = (c, fn ctxt => fn show_sorts => fn T => fn ts =>
    1.14 +    if not (null ts) orelse T = dummyT
    1.15 +      orelse not (Config.get ctxt show_types) andalso can Term.dest_Type T
    1.16      then raise Match
    1.17      else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
    1.18  in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;