diff -r 340df9f3491f -r 22f665a2e91c src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Probability/Information.thy	Mon Sep 12 07:55:43 2011 +0200
@@ -35,7 +35,7 @@
   have "convex_on {0 <..} (\<lambda> x. - log b x)"
     by (rule minus_log_convex[OF `b > 1`])
   hence "- log b (\<Sum> i \<in> s. a i * y i) \<le> (\<Sum> i \<in> s. a i * - log b (y i))"
-    using convex_on_setsum[of _ _ "\<lambda> x. - log b x"] assms pos_is_convex by fastsimp
+    using convex_on_setsum[of _ _ "\<lambda> x. - log b x"] assms pos_is_convex by fastforce
   thus ?thesis by (auto simp add:setsum_negf le_imp_neg_le)
 qed
 
@@ -1327,7 +1327,7 @@
   shows "finite (g`A)"
 proof -
   from subvimage_translator_image[OF svi]
-  obtain h where "g`A = h`f`A" by fastsimp
+  obtain h where "g`A = h`f`A" by fastforce
   with fin show "finite (g`A)" by simp
 qed