src/HOL/HOLCF/Adm.thy

--- a/src/HOL/HOLCF/Adm.thy	Sun Apr 24 21:31:14 2016 +0200
+++ b/src/HOL/HOLCF/Adm.thy	Mon Apr 25 16:09:26 2016 +0200
@@ -61,7 +61,7 @@
   assumes P: "\<forall>i. \<exists>j\<ge>i. P (Y j)"
   shows "P (\<Squnion>i. Y i)"
 proof -
-  def f \<equiv> "\<lambda>i. LEAST j. i \<le> j \<and> P (Y j)"
+  define f where "f i = (LEAST j. i \<le> j \<and> P (Y j))" for i
   have chain': "chain (\<lambda>i. Y (f i))"
     unfolding f_def
     apply (rule chainI)