diff -r f30e941b4512 -r 6b1c0a80a57a src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Tue Mar 13 16:40:06 2012 +0100
+++ b/src/HOL/Probability/Information.thy	Tue Mar 13 16:56:56 2012 +0100
@@ -823,7 +823,7 @@
   interpret S: prob_space "S\<lparr> measure := ereal\<circ>distribution X \<rparr>"
     using distribution_prob_space[OF X] .
   from A show "S.\<mu>' A = distribution X A"
-    unfolding S.\<mu>'_def by (simp add: distribution_def_raw \<mu>'_def)
+    unfolding S.\<mu>'_def by (simp add: distribution_def [abs_def] \<mu>'_def)
 qed
 
 lemma (in information_space) entropy_uniform_max: