change formula for enumerating scopes
authorblanchet
Tue, 03 Aug 2010 18:27:21 +0200
changeset 38187 fd28328daf73
parent 38186 c28018f5a1d6
child 38188 7f12a03c513c
change formula for enumerating scopes
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 =