src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy

--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Wed Oct 10 12:12:28 2012 +0200
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Wed Oct 10 12:12:29 2012 +0200
@@ -306,7 +306,6 @@
      log b ((\<P>(X ; Y) {(x,y)}) / (\<P>(Y) {y}))))"
   apply (subst conditional_entropy_eq[OF
     simple_distributedI[OF simple_function_finite refl]
-    simple_function_finite
     simple_distributedI[OF simple_function_finite refl]])
   unfolding space_point_measure
 proof -