diff -r 1a20fd9cf281 -r eb4ddd18d635 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Sun Apr 24 21:31:14 2016 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Mon Apr 25 16:09:26 2016 +0200
@@ -110,7 +110,8 @@
            2: "\<And>x n. P n x \<Longrightarrow> \<exists>y. P (Suc n) y \<and> Q n x y"
   shows "\<exists>f. \<forall>n. P n (f n) \<and> Q n (f n) (f (Suc n))"
 proof (intro exI allI conjI)
-  fix n def f \<equiv> "rec_nat (SOME x. P 0 x) (\<lambda>n x. SOME y. P (Suc n) y \<and> Q n x y)"
+  fix n
+  define f where "f = rec_nat (SOME x. P 0 x) (\<lambda>n x. SOME y. P (Suc n) y \<and> Q n x y)"
   have "P 0 (f 0)" "\<And>n. P n (f n) \<Longrightarrow> P (Suc n) (f (Suc n)) \<and> Q n (f n) (f (Suc n))"
     using someI_ex[OF 1] someI_ex[OF 2] by (simp_all add: f_def)
   then show "P n (f n)" "Q n (f n) (f (Suc n))"
@@ -309,8 +310,8 @@
   shows "\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S"
   \<comment> \<open>Courtesy of Stephan Merz\<close>
 proof -
-  def Sseq \<equiv> "rec_nat S (\<lambda>n T. T - {SOME e. e \<in> T})"
-  def pick \<equiv> "\<lambda>n. (SOME e. e \<in> Sseq n)"
+  define Sseq where "Sseq = rec_nat S (\<lambda>n T. T - {SOME e. e \<in> T})"
+  define pick where "pick n = (SOME e. e \<in> Sseq n)" for n
   { fix n have "Sseq n \<subseteq> S" "\<not> finite (Sseq n)" by (induct n) (auto simp add: Sseq_def inf) }
   moreover then have *: "\<And>n. pick n \<in> Sseq n"
     unfolding pick_def by (subst (asm) finite.simps) (auto simp add: ex_in_conv intro: someI_ex)
@@ -746,7 +747,7 @@
     then show False by simp
   qed
   then obtain n where n: "f n = f (Suc n)" ..
-  def N \<equiv> "LEAST n. f n = f (Suc n)"
+  define N where "N = (LEAST n. f n = f (Suc n))"
   have N: "f N = f (Suc N)"
     unfolding N_def using n by (rule LeastI)
   show ?thesis