diff -r 915da29bf5d9 -r 7e741e22d7fc src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/Probability/Information.thy	Thu Jun 25 23:33:47 2015 +0200
@@ -1022,11 +1022,12 @@
     Pxyz x * log b (Pxz (fst x, snd (snd x)) / (Px (fst x) * Pz (snd (snd x)))) =
     Pxyz x * log b (Pxyz x * Pz (snd (snd x)) / (Pxz (fst x, snd (snd x)) * Pyz (snd x))) "
   proof eventually_elim
-    case (goal1 x)
+    case (elim x)
     show ?case
     proof cases
       assume "Pxyz x \<noteq> 0"
-      with goal1 have "0 < Px (fst x)" "0 < Pz (snd (snd x))" "0 < Pxz (fst x, snd (snd x))" "0 < Pyz (snd x)" "0 < Pxyz x"
+      with elim have "0 < Px (fst x)" "0 < Pz (snd (snd x))" "0 < Pxz (fst x, snd (snd x))"
+        "0 < Pyz (snd x)" "0 < Pxyz x"
         by auto
       then show ?thesis
         using b_gt_1 by (simp add: log_simps less_imp_le field_simps)
@@ -1252,11 +1253,12 @@
     Pxyz x * log b (Pxz (fst x, snd (snd x)) / (Px (fst x) * Pz (snd (snd x)))) =
     Pxyz x * log b (Pxyz x * Pz (snd (snd x)) / (Pxz (fst x, snd (snd x)) * Pyz (snd x))) "
   proof eventually_elim
-    case (goal1 x)
+    case (elim x)
     show ?case
     proof cases
       assume "Pxyz x \<noteq> 0"
-      with goal1 have "0 < Px (fst x)" "0 < Pz (snd (snd x))" "0 < Pxz (fst x, snd (snd x))" "0 < Pyz (snd x)" "0 < Pxyz x"
+      with elim have "0 < Px (fst x)" "0 < Pz (snd (snd x))" "0 < Pxz (fst x, snd (snd x))"
+        "0 < Pyz (snd x)" "0 < Pxyz x"
         by auto
       then show ?thesis
         using b_gt_1 by (simp add: log_simps less_imp_le field_simps)
@@ -1730,11 +1732,11 @@
     Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x)))"
     (is "AE x in _. ?f x = ?g x")
   proof eventually_elim
-    case (goal1 x)
+    case (elim x)
     show ?case
     proof cases
       assume "Pxy x \<noteq> 0"
-      with goal1 have "0 < Px (fst x)" "0 < Py (snd x)" "0 < Pxy x"
+      with elim have "0 < Px (fst x)" "0 < Py (snd x)" "0 < Pxy x"
         by auto
       then show ?thesis
         using b_gt_1 by (simp add: log_simps less_imp_le field_simps)