--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Feb 23 11:05:32 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Feb 23 12:14:29 2010 +0100
@@ -1091,7 +1091,8 @@
else
accum |> fold (add_nondef_axiom depth)
(nondef_props_for_const thy false nondef_table x)
- |> is_funky_typedef thy (range_type T)
+ |> (is_funky_typedef thy (range_type T) orelse
+ range_type T = nat_T)
? fold (add_maybe_def_axiom depth)
(nondef_props_for_const thy true
(extra_table def_table s) x)
@@ -1101,7 +1102,8 @@
else
accum |> fold (add_nondef_axiom depth)
(nondef_props_for_const thy false nondef_table x)
- |> is_funky_typedef thy (range_type T)
+ |> (is_funky_typedef thy (range_type T) orelse
+ range_type T = nat_T)
? fold (add_maybe_def_axiom depth)
(nondef_props_for_const thy true
(extra_table def_table s) x)