--- 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
--- 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)