1.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Dec 05 09:23:59 2013 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Dec 05 13:22:00 2013 +0100
     1.3 @@ -1545,16 +1545,16 @@
     1.4    |> Typ_Graph.strong_conn
     1.5    |> map (fn keys => filter (member (op =) keys o fst) nfa)
     1.6  
     1.7 -fun acyclicity_axiom_for_datatype (kk as {kk_no, kk_intersect, ...}) nfa
     1.8 -                                  start_T =
     1.9 -  kk_no (kk_intersect
    1.10 -             (loop_path_rel_expr kk nfa (pull start_T (map fst nfa)) start_T)
    1.11 -             KK.Iden)
    1.12  (* Cycle breaking in the bounds takes care of singly recursive datatypes, hence
    1.13     the first equation. *)
    1.14 -fun acyclicity_axioms_for_datatypes _ [_] = []
    1.15 -  | acyclicity_axioms_for_datatypes kk nfas =
    1.16 -    maps (fn nfa => map (acyclicity_axiom_for_datatype kk nfa o fst) nfa) nfas
    1.17 +fun acyclicity_axioms_for_datatype _ [_] _ = []
    1.18 +  | acyclicity_axioms_for_datatype (kk as {kk_no, kk_intersect, ...}) nfa
    1.19 +                                   start_T =
    1.20 +    [kk_no (kk_intersect
    1.21 +                (loop_path_rel_expr kk nfa (pull start_T (map fst nfa)) start_T)
    1.22 +                KK.Iden)]
    1.23 +fun acyclicity_axioms_for_datatypes kk =
    1.24 +  maps (fn nfa => maps (acyclicity_axioms_for_datatype kk nfa o fst) nfa)
    1.25  
    1.26  fun atom_equation_for_nut ofs kk (u, j) =
    1.27    let val dummy_u = RelReg (0, type_of u, rep_of u) in