# HG changeset patch
# User blanchet
# Date 1280957247 -7200
# Node ID a8cef06e0480b615a72082a5ce10c2245494f9ce
# Parent  a9877c14550fa142c94ceeea82aeb81cfc72042b
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

diff -r a9877c14550f -r a8cef06e0480 src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- 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)))