src/ZF/ex/Primes.thy

--- a/src/ZF/ex/Primes.thy	Wed Jul 02 17:34:45 2014 +0200
+++ b/src/ZF/ex/Primes.thy	Wed Jun 11 14:24:23 2014 +1000
@@ -71,7 +71,7 @@
 
 lemma dvd_mult_right: "[|(i#*j) dvd k; j \<in> nat|] ==> j dvd k"
 apply (simp add: divides_def, clarify)
-apply (rule_tac x = "i#*k" in bexI)
+apply (rule_tac x = "i#*ka" in bexI)
 apply (simp add: mult_ac)
 apply (rule mult_type)
 done