1.1 --- a/NEWS	Thu Dec 05 09:23:59 2013 +0100
     1.2 +++ b/NEWS	Thu Dec 05 13:22:00 2013 +0100
     1.3 @@ -520,6 +520,10 @@
     1.4      sets ~> set
     1.5  IMCOMPATIBILITY.
     1.6  
     1.7 +* Nitpick:
     1.8 +  - Fixed soundness bug whereby mutually recursive datatypes could take
     1.9 +    infinite values.
    1.10 +
    1.11  
    1.12  *** ML ***
    1.13  

     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Dec 05 09:23:59 2013 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Dec 05 13:22:00 2013 +0100
     2.3 @@ -1545,16 +1545,16 @@
     2.4    |> Typ_Graph.strong_conn
     2.5    |> map (fn keys => filter (member (op =) keys o fst) nfa)
     2.6  
     2.7 -fun acyclicity_axiom_for_datatype (kk as {kk_no, kk_intersect, ...}) nfa
     2.8 -                                  start_T =
     2.9 -  kk_no (kk_intersect
    2.10 -             (loop_path_rel_expr kk nfa (pull start_T (map fst nfa)) start_T)
    2.11 -             KK.Iden)
    2.12  (* Cycle breaking in the bounds takes care of singly recursive datatypes, hence
    2.13     the first equation. *)
    2.14 -fun acyclicity_axioms_for_datatypes _ [_] = []
    2.15 -  | acyclicity_axioms_for_datatypes kk nfas =
    2.16 -    maps (fn nfa => map (acyclicity_axiom_for_datatype kk nfa o fst) nfa) nfas
    2.17 +fun acyclicity_axioms_for_datatype _ [_] _ = []
    2.18 +  | acyclicity_axioms_for_datatype (kk as {kk_no, kk_intersect, ...}) nfa
    2.19 +                                   start_T =
    2.20 +    [kk_no (kk_intersect
    2.21 +                (loop_path_rel_expr kk nfa (pull start_T (map fst nfa)) start_T)
    2.22 +                KK.Iden)]
    2.23 +fun acyclicity_axioms_for_datatypes kk =
    2.24 +  maps (fn nfa => maps (acyclicity_axioms_for_datatype kk nfa o fst) nfa)
    2.25  
    2.26  fun atom_equation_for_nut ofs kk (u, j) =
    2.27    let val dummy_u = RelReg (0, type_of u, rep_of u) in