# HG changeset patch
# User blanchet
# Date 1300530143 -3600
# Node ID 0c39117616803e6a6b13f9200f60dec89da2c339
# Parent  3c029ef9e0f290ec6aad73e6d8d96c08100a30c5
ignore "need" axioms for "nat"-like types

diff -r 3c029ef9e0f2 -r 0c3911761680 src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Fri Mar 18 22:55:28 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Sat Mar 19 11:22:23 2011 +0100
@@ -301,8 +301,11 @@
     raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u])
 
 fun is_datatype_nat_like ({typ, constrs, ...} : datatype_spec) =
-  case constrs |> map (snd o #const) |> List.partition is_fun_type of
-    ([Type (_, Ts1)], [T2]) => forall (curry (op =) typ) (T2 :: Ts1)
+  case constrs of
+    [_, _] =>
+    (case constrs |> map (snd o #const) |> List.partition is_fun_type of
+       ([Type (_, Ts1)], [T2]) => forall (curry (op =) typ) (T2 :: Ts1)
+     | _ => false)
   | _ => false
 
 fun needed_values need_vals T =
@@ -1520,7 +1523,7 @@
 
 fun needed_values_for_datatype [] _ _ = SOME []
   | needed_values_for_datatype need_us ofs
-        ({typ, card, constrs, ...} : datatype_spec) =
+                               (dtype as {typ, card, constrs, ...}) =
     let
       fun aux (u as Construct (FreeRel (_, _, _, s) :: _, T, _, us)) =
           fold aux us
@@ -1548,7 +1551,11 @@
                    accum)
         | aux _ = I
     in
-      SOME (index_seq 0 card, []) |> fold aux need_us |> Option.map (rev o snd)
+      if is_datatype_nat_like dtype then
+        SOME []
+      else
+        SOME (index_seq 0 card, [])
+        |> fold aux need_us |> Option.map (rev o snd)
     end
 
 fun needed_value_axioms_for_datatype _ _ NONE = [KK.False]