src/HOL/Groups.thy
changeset 42247 12fe41a92cd5
parent 42245 29e3967550d5
child 42248 04bffad68aa4
     1.1 --- a/src/HOL/Groups.thy	Wed Apr 06 13:27:59 2011 +0200
     1.2 +++ b/src/HOL/Groups.thy	Wed Apr 06 13:33:46 2011 +0200
     1.3 @@ -125,13 +125,13 @@
     1.4  simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
     1.5  
     1.6  typed_print_translation (advanced) {*
     1.7 -let
     1.8 -  fun tr' c = (c, fn ctxt => fn show_sorts => fn T => fn ts =>
     1.9 -    if not (null ts) orelse T = dummyT
    1.10 -      orelse not (Config.get ctxt show_types) andalso can Term.dest_Type T
    1.11 -    then raise Match
    1.12 -    else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax_Phases.term_of_typ show_sorts T);
    1.13 -in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
    1.14 +  let
    1.15 +    fun tr' c = (c, fn ctxt => fn T => fn ts =>
    1.16 +      if not (null ts) orelse T = dummyT
    1.17 +        orelse not (Config.get ctxt show_types) andalso can Term.dest_Type T
    1.18 +      then raise Match
    1.19 +      else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax_Phases.term_of_typ ctxt T);
    1.20 +  in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
    1.21  *} -- {* show types that are presumably too general *}
    1.22  
    1.23  class plus =