diff -r 1502f2410d8b -r a4c0de1df3d8 src/HOL/ex/Parallel_Example.thy
--- a/src/HOL/ex/Parallel_Example.thy	Thu Oct 15 12:39:51 2015 +0200
+++ b/src/HOL/ex/Parallel_Example.thy	Sat Oct 17 13:18:43 2015 +0200
@@ -61,7 +61,7 @@
 function factorise_from :: "nat \<Rightarrow> nat \<Rightarrow> nat list" where
   "factorise_from k n = (if 1 < k \<and> k \<le> n
     then
-      let (q, r) = divmod_nat n k 
+      let (q, r) = Divides.divmod_nat n k 
       in if r = 0 then k # factorise_from k q
         else factorise_from (Suc k) n
     else [])" 
@@ -105,4 +105,3 @@
 value "computation_parallel ()"
 
 end
-