# HG changeset patch
# User blanchet
# Date 1280749702 -7200
# Node ID 824e940a3dd0bdfe52a0b338d9c6d021dda03f8a
# Parent  c1cf80763eff8b8cde1f81fdc01c8c1ec7f2a798
minor symmetry breaking for codatatypes like llist

diff -r c1cf80763eff -r 824e940a3dd0 src/HOL/Tools/Nitpick/nitpick_scope.ML
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Mon Aug 02 12:36:50 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Mon Aug 02 13:48:22 2010 +0200
@@ -387,7 +387,7 @@
 fun domain_card max card_assigns =
   Integer.prod o map (bounded_card_of_type max max card_assigns) o binder_types
 
-fun add_constr_spec (card_assigns, max_assigns) co card sum_dom_cards
+fun add_constr_spec (card_assigns, max_assigns) acyclic card sum_dom_cards
                     num_self_recs num_non_self_recs (self_rec, x as (_, T))
                     constrs =
   let
@@ -398,7 +398,7 @@
         let val delta = next_delta () in
           {delta = delta, epsilon = delta, exclusive = true, total = false}
         end
-      else if not co andalso num_self_recs > 0 then
+      else if num_self_recs > 0 then
         (if num_self_recs = 1 andalso num_non_self_recs = 1 then
            if self_rec then
              case constrs of
@@ -407,7 +407,7 @@
              | _ => raise SAME ()
            else
              if domain_card 2 card_assigns T = 1 then
-               {delta = 0, epsilon = 1, exclusive = true, total = true}
+               {delta = 0, epsilon = 1, exclusive = acyclic, total = acyclic}
              else
                raise SAME ()
          else
@@ -457,8 +457,8 @@
     fun sum_dom_cards max =
       map (domain_card max card_assigns o snd) xs |> Integer.sum
     val constrs =
-      fold_rev (add_constr_spec desc co card sum_dom_cards num_self_recs
-                                num_non_self_recs)
+      fold_rev (add_constr_spec desc (not co andalso standard) card
+                                sum_dom_cards num_self_recs num_non_self_recs)
                (sort (bool_ord o swap o pairself fst) (self_recs ~~ xs)) []
   in
     {typ = T, card = card, co = co, standard = standard, self_rec = self_rec,