src/HOL/Probability/Measure_Space.thy

--- a/src/HOL/Probability/Measure_Space.thy	Sun Apr 24 21:31:14 2016 +0200
+++ b/src/HOL/Probability/Measure_Space.thy	Mon Apr 25 16:09:26 2016 +0200
@@ -567,7 +567,7 @@
     by simp
 next
   assume "infinite I"
-  def L \<equiv> "\<lambda>n. LEAST i. i \<in> I \<and> i \<ge> n"
+  define L where "L n = (LEAST i. i \<in> I \<and> i \<ge> n)" for n
   have L: "L n \<in> I \<and> n \<le> L n" for n
     unfolding L_def
   proof (rule LeastI_ex)