do not drop arguments to 0, 1
authorhaftmann
Wed Feb 18 19:18:31 2009 +0100 (2009-02-18)
changeset 299687171f3f058b6
parent 29967 f14ce13c73c1
child 29969 9dbb046136d0
do not drop arguments to 0, 1
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Wed Feb 18 13:39:16 2009 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Feb 18 19:18:31 2009 +0100
     1.3 @@ -290,7 +290,7 @@
     1.4  typed_print_translation {*
     1.5  let
     1.6    fun tr' c = (c, fn show_sorts => fn T => fn ts =>
     1.7 -    if T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match
     1.8 +    if (not o null) ts orelse T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match
     1.9      else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
    1.10  in map tr' [@{const_syntax HOL.one}, @{const_syntax HOL.zero}] end;
    1.11  *} -- {* show types that are presumably too general *}