1.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Fri Mar 18 22:55:28 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Sat Mar 19 11:22:23 2011 +0100
     1.3 @@ -301,8 +301,11 @@
     1.4      raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u])
     1.5  
     1.6  fun is_datatype_nat_like ({typ, constrs, ...} : datatype_spec) =
     1.7 -  case constrs |> map (snd o #const) |> List.partition is_fun_type of
     1.8 -    ([Type (_, Ts1)], [T2]) => forall (curry (op =) typ) (T2 :: Ts1)
     1.9 +  case constrs of
    1.10 +    [_, _] =>
    1.11 +    (case constrs |> map (snd o #const) |> List.partition is_fun_type of
    1.12 +       ([Type (_, Ts1)], [T2]) => forall (curry (op =) typ) (T2 :: Ts1)
    1.13 +     | _ => false)
    1.14    | _ => false
    1.15  
    1.16  fun needed_values need_vals T =
    1.17 @@ -1520,7 +1523,7 @@
    1.18  
    1.19  fun needed_values_for_datatype [] _ _ = SOME []
    1.20    | needed_values_for_datatype need_us ofs
    1.21 -        ({typ, card, constrs, ...} : datatype_spec) =
    1.22 +                               (dtype as {typ, card, constrs, ...}) =
    1.23      let
    1.24        fun aux (u as Construct (FreeRel (_, _, _, s) :: _, T, _, us)) =
    1.25            fold aux us
    1.26 @@ -1548,7 +1551,11 @@
    1.27                     accum)
    1.28          | aux _ = I
    1.29      in
    1.30 -      SOME (index_seq 0 card, []) |> fold aux need_us |> Option.map (rev o snd)
    1.31 +      if is_datatype_nat_like dtype then
    1.32 +        SOME []
    1.33 +      else
    1.34 +        SOME (index_seq 0 card, [])
    1.35 +        |> fold aux need_us |> Option.map (rev o snd)
    1.36      end
    1.37  
    1.38  fun needed_value_axioms_for_datatype _ _ NONE = [KK.False]