src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy

   assumes "length w = length v"
   shows "(\<Sum>x\<leftarrow>sparsify w. (\<lambda>(i, x). v ! i) x * snd x) = scalar_product v w"
     (is "(\<Sum>x\<leftarrow>_. ?f x) = _")
   unfolding sparsify_def scalar_product_def
   using assms sum_list_map_filter[where f="?f" and P="\<lambda> i. snd i \<noteq> (0::'a)"]
-  by (simp add: sum_list_setsum)
+  by (simp add: sum_list_sum)
 *)
 definition [simp]: "unzip w = (map fst w, map snd w)"
 
 primrec insert :: "('a \<Rightarrow> 'b :: linorder) => 'a \<Rightarrow> 'a list => 'a list" where
   "insert f x [] = [x]" |