1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon May 31 17:41:06 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon May 31 18:00:28 2010 +0200
     1.3 @@ -1397,8 +1397,10 @@
     1.4                            if slack then
     1.5                              I
     1.6                            else
     1.7 -                            raise NOT_SUPPORTED ("too much polymorphism in \
     1.8 -                                                 \axiom involving " ^ quote s))
     1.9 +                            raise NOT_SUPPORTED
    1.10 +                                      ("too much polymorphism in axiom \"" ^
    1.11 +                                       Syntax.string_of_term_global thy t ^
    1.12 +                                       "\" involving " ^ quote s))
    1.13          else
    1.14            ys
    1.15        | aux _ ys = ys

     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon May 31 17:41:06 2010 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon May 31 18:00:28 2010 +0200
     2.3 @@ -955,6 +955,8 @@
     2.4                                                (Const (mate_of_rep_fun thy x))
     2.5                         |> fold (add_def_axiom depth)
     2.6                                 (inverse_axioms_for_rep_fun thy x)
     2.7 +             else if s = @{const_name TYPE} then
     2.8 +               accum
     2.9               else
    2.10                 accum |> user_axioms <> SOME false
    2.11                          ? fold (add_nondef_axiom depth)