# HG changeset patch
# User blanchet
# Date 1275321628 -7200
# Node ID e01c1fe245cda419a25d8e3e703493eefc13de62
# Parent  47d1ee50205b44bf19bce1e362cc64a1abca29b9
don't include any axioms for "TYPE" in Nitpick

diff -r 47d1ee50205b -r e01c1fe245cd src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon May 31 17:41:06 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon May 31 18:00:28 2010 +0200
@@ -1397,8 +1397,10 @@
                           if slack then
                             I
                           else
-                            raise NOT_SUPPORTED ("too much polymorphism in \
-                                                 \axiom involving " ^ quote s))
+                            raise NOT_SUPPORTED
+                                      ("too much polymorphism in axiom \"" ^
+                                       Syntax.string_of_term_global thy t ^
+                                       "\" involving " ^ quote s))
         else
           ys
       | aux _ ys = ys
diff -r 47d1ee50205b -r e01c1fe245cd src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon May 31 17:41:06 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon May 31 18:00:28 2010 +0200
@@ -955,6 +955,8 @@
                                               (Const (mate_of_rep_fun thy x))
                        |> fold (add_def_axiom depth)
                                (inverse_axioms_for_rep_fun thy x)
+             else if s = @{const_name TYPE} then
+               accum
              else
                accum |> user_axioms <> SOME false
                         ? fold (add_nondef_axiom depth)