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]