diff -r e5b84854baa4 -r 6e6eeef63589 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Jun 26 14:26:03 2017 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Jun 26 16:59:44 2017 +0100
@@ -1673,7 +1673,7 @@
         assume "(x, k) \<in> p'"
         then have "\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> k = i \<inter> l"
           unfolding p'_def by auto
-        then guess i l by (elim exE) note il=conjunctD4[OF this]
+        then obtain i l where il: "x \<in> i" "i \<in> d" "(x, l) \<in> p" "k = i \<inter> l" by blast
         show "x \<in> k" and "k \<subseteq> cbox a b"
           using p'(2-3)[OF il(3)] il by auto
         show "\<exists>a b. k = cbox a b"
@@ -1687,12 +1687,12 @@
         assume "(x1, k1) \<in> p'"
         then have "\<exists>i l. x1 \<in> i \<and> i \<in> d \<and> (x1, l) \<in> p \<and> k1 = i \<inter> l"
           unfolding p'_def by auto
-        then guess i1 l1 by (elim exE) note il1=conjunctD4[OF this]
+        then obtain i1 l1 where il1: "x1 \<in> i1" "i1 \<in> d" "(x1, l1) \<in> p" "k1 = i1 \<inter> l1" by blast
         fix x2 k2
         assume "(x2,k2)\<in>p'"
         then have "\<exists>i l. x2 \<in> i \<and> i \<in> d \<and> (x2, l) \<in> p \<and> k2 = i \<inter> l"
           unfolding p'_def by auto
-        then guess i2 l2 by (elim exE) note il2=conjunctD4[OF this]
+        then obtain i2 l2 where il2: "x2 \<in> i2" "i2 \<in> d" "(x2, l2) \<in> p" "k2 = i2 \<inter> l2" by blast
         assume "(x1, k1) \<noteq> (x2, k2)"
         then have "interior i1 \<inter> interior i2 = {} \<or> interior l1 \<inter> interior l2 = {}"
           using d'(5)[OF il1(2) il2(2)] p'(5)[OF il1(3) il2(3)]
@@ -1768,7 +1768,7 @@
         assume "(x, k) \<in> p'"
         then have "\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> k = i \<inter> l"
           unfolding p'_def by auto
-        then guess i l by (elim exE) note il=conjunctD4[OF this]
+        then obtain i l where il: "x \<in> i" "i \<in> d" "(x, l) \<in> p" "k = i \<inter> l" by blast
         then show "\<exists>y i l. (x, k) = (y, i \<inter> l) \<and> (y, l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}"
           apply (rule_tac x=x in exI)
           apply (rule_tac x=i in exI)