diff -r 1a20fd9cf281 -r eb4ddd18d635 src/HOL/Number_Theory/Eratosthenes.thy
--- a/src/HOL/Number_Theory/Eratosthenes.thy	Sun Apr 24 21:31:14 2016 +0200
+++ b/src/HOL/Number_Theory/Eratosthenes.thy	Mon Apr 25 16:09:26 2016 +0200
@@ -96,7 +96,7 @@
     with A B C show ?thesis by simp
   next
     case False
-    def m \<equiv> "Suc n"
+    define m where "m = Suc n"
     then have "m > 0" by simp
     from False have "n > 0" by simp
     from A obtain q where q: "Suc (Suc a) = Suc n * q" by (rule dvdE)
@@ -133,7 +133,8 @@
       enumerate_Suc_eq in_set_enumerate_eq less_eq_dvd_minus)
 next
   case 3
-  { def v \<equiv> "Suc m" and w \<equiv> "Suc n"
+  { define v where "v = Suc m"
+    define w where "w = Suc n"
     fix q
     assume "m + n \<le> q"
     then obtain r where q: "q = m + n + r" by (auto simp add: le_iff_add)
@@ -359,7 +360,7 @@
   have "List.find (\<lambda>p. p \<ge> m) (primes_upto n) = Some (smallest_prime_beyond m)"
     if assms: "m \<le> p" "prime p" "p \<le> n" for p
   proof -
-    def A \<equiv> "{p. p \<le> n \<and> prime p \<and> m \<le> p}"
+    define A where "A = {p. p \<le> n \<and> prime p \<and> m \<le> p}"
     from assms have "smallest_prime_beyond m \<le> p"
       by (auto intro: smallest_prime_beyond_smallest)
     from this \<open>p \<le> n\<close> have *: "smallest_prime_beyond m \<le> n"