# HG changeset patch
# User haftmann
# Date 1234981111 -3600
# Node ID 7171f3f058b65bc52b783bb53b717bba0f7b65fa
# Parent  f14ce13c73c18aa64c8fffc04674952cee408365
do not drop arguments to 0, 1

diff -r f14ce13c73c1 -r 7171f3f058b6 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Feb 18 13:39:16 2009 +0100
+++ b/src/HOL/HOL.thy	Wed Feb 18 19:18:31 2009 +0100
@@ -290,7 +290,7 @@
 typed_print_translation {*
 let
   fun tr' c = (c, fn show_sorts => fn T => fn ts =>
-    if T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match
+    if (not o null) ts orelse T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match
     else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
 in map tr' [@{const_syntax HOL.one}, @{const_syntax HOL.zero}] end;
 *} -- {* show types that are presumably too general *}