--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu Feb 04 16:50:26 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Fri Feb 05 11:14:34 2010 +0100
@@ -426,16 +426,21 @@
{delta = delta, epsilon = delta, exclusive = true, total = false}
end
else if not co andalso num_self_recs > 0 then
- if not self_rec andalso num_non_self_recs = 1 andalso
- domain_card 2 card_assigns T = 1 then
- {delta = 0, epsilon = 1,
- exclusive = (s = @{const_name Nil} andalso length constrs = 2),
- total = true}
- else if s = @{const_name Cons} andalso
- num_self_recs + num_non_self_recs = 2 then
- {delta = 1, epsilon = card, exclusive = true, total = false}
- else
- {delta = 0, epsilon = card, exclusive = false, total = false}
+ (if num_self_recs = 1 andalso num_non_self_recs = 1 then
+ if self_rec then
+ case constrs of
+ [{delta = 0, epsilon = 1, exclusive = true, ...}] =>
+ {delta = 1, epsilon = card, exclusive = true, total = false}
+ | _ => raise SAME ()
+ else
+ if domain_card 2 card_assigns T = 1 then
+ {delta = 0, epsilon = 1, exclusive = true, total = true}
+ else
+ raise SAME ()
+ else
+ raise SAME ())
+ handle SAME () =>
+ {delta = 0, epsilon = card, exclusive = false, total = false}
else if card = sum_dom_cards (card + 1) then
let val delta = next_delta () in
{delta = delta, epsilon = delta + domain_card card card_assigns T,
@@ -473,7 +478,8 @@
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) (self_recs ~~ xs) []
+ num_non_self_recs)
+ (sort (bool_ord o swap o pairself fst) (self_recs ~~ xs)) []
in
{typ = T, card = card, co = co, complete = complete, concrete = concrete,
deep = deep, constrs = constrs}