diff -r 430d74089d4d -r 93c6f0da5c70 src/Doc/Tutorial/Rules/Force.thy
--- a/src/Doc/Tutorial/Rules/Force.thy	Sun Oct 16 09:31:04 2016 +0200
+++ b/src/Doc/Tutorial/Rules/Force.thy	Sun Oct 16 09:31:05 2016 +0200
@@ -6,7 +6,7 @@
 
 lemma div_mult_self_is_m: 
       "0<n \<Longrightarrow> (m*n) div n = (m::nat)"
-apply (insert mod_div_equality [of "m*n" n])
+apply (insert div_mult_mod_eq [of "m*n" n])
 apply simp
 done