diff -r 8031d099379a -r 9f9f696fc4e8 src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Sun Aug 01 15:51:25 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Sun Aug 01 16:35:25 2010 +0200
@@ -786,6 +786,7 @@
    break cycles; otherwise, we may end up with two incompatible symmetry
    breaking orders, leading to spurious models. *)
 fun should_tabulate_suc_for_type dtypes T =
+  is_asymmetric_nondatatype T orelse
   case datatype_spec dtypes T of
     SOME {self_rec, ...} => self_rec
   | NONE => false
@@ -908,7 +909,10 @@
                                         dtypes)
          (dtypes |> filter is_datatype_good_and_old
                  |> filter (fn {constrs = [_], ...} => false
-                             | {card, ...} => card >= min_sym_break_card)
+                             | {card, constrs, ...} =>
+                               card >= min_sym_break_card andalso
+                               forall (forall (not o is_higher_order_type)
+                                       o binder_types o snd o #const) constrs)
                  |> (fn dtypes' =>
                         dtypes'
                         |> length dtypes' > datatype_sym_break