src/HOL/ex/Parallel_Example.thy

--- a/src/HOL/ex/Parallel_Example.thy	Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/ex/Parallel_Example.thy	Thu Sep 15 11:48:20 2016 +0200
@@ -9,7 +9,7 @@
 subsubsection \<open>Fragments of the harmonic series\<close>
 
 definition harmonic :: "nat \<Rightarrow> rat" where
-  "harmonic n = listsum (map (\<lambda>n. 1 / of_nat n) [1..<n])"
+  "harmonic n = sum_list (map (\<lambda>n. 1 / of_nat n) [1..<n])"
 
 
 subsubsection \<open>The sieve of Erathostenes\<close>