# HG changeset patch
# User blanchet
# Date 1280852841 -7200
# Node ID fd28328daf7314d3f5500405e15dabd710a20b61
# Parent  c28018f5a1d657611c267ffe168210af30a225b8
change formula for enumerating scopes

diff -r c28018f5a1d6 -r fd28328daf73 src/HOL/Tools/Nitpick/nitpick_scope.ML
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Aug 03 18:14:44 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Aug 03 18:27:21 2010 +0200
@@ -282,10 +282,10 @@
         if k < sync_threshold andalso forall (curry (op =) k) ks then
           k - sync_threshold
         else
-          Integer.product (map (fn k => (k + linearity) * (k + linearity))
-                               (k :: ks))
+          k :: ks |> map (fn k => (k + linearity) * (k + linearity))
+                  |> Integer.sum
   in
-    all_combinations #> map cost #> sort (int_ord o pairself fst) #> map snd
+    all_combinations #> map (`cost) #> sort (int_ord o pairself fst) #> map snd
   end
 
 fun is_self_recursive_constr_type T =