Cycle breaking in the bounds takes care of singly recursive datatypes, so we don't need to do it again;
the effect of removing the constraint varies on problem to problem, but it tends to be overwhelmingly negative in conjuction with the new datatype sym breaking stuff at high cardinalities

--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Aug 04 22:47:52 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Aug 04 23:27:27 2010 +0200
@@ -739,8 +739,11 @@
   kk_no (kk_intersect
              (loop_path_rel_expr kk nfa (pull start_T (map fst nfa)) start_T)
              KK.Iden)
-fun acyclicity_axioms_for_datatypes kk nfas =
-  maps (fn nfa => map (acyclicity_axiom_for_datatype kk nfa o fst) nfa) nfas
+(* Cycle breaking in the bounds takes care of singly recursive datatypes, hence
+   the first equation. *)
+fun acyclicity_axioms_for_datatypes kk [_] = []
+  | acyclicity_axioms_for_datatypes kk nfas =
+    maps (fn nfa => map (acyclicity_axiom_for_datatype kk nfa o fst) nfa) nfas
 
 fun all_ge ({kk_join, kk_reflexive_closure, ...} : kodkod_constrs) z r =
   kk_join r (kk_reflexive_closure (KK.Rel (suc_rel_for_atom_seq z)))