diff -r 33db4b7189af -r 3793c3a11378 src/HOL/ex/Gauge_Integration.thy
--- a/src/HOL/ex/Gauge_Integration.thy	Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/ex/Gauge_Integration.thy	Fri Mar 22 10:41:43 2013 +0100
@@ -97,11 +97,7 @@
   assumes 2: "\<And>a b c. \<lbrakk>P a b; P b c; a \<le> b; b \<le> c\<rbrakk> \<Longrightarrow> P a c"
   assumes 3: "\<And>x. \<exists>d>0. \<forall>a b. a \<le> x & x \<le> b & (b-a) < d \<longrightarrow> P a b"
   shows "P a b"
-apply (subgoal_tac "split P (a,b)", simp)
-apply (rule lemma_BOLZANO [OF _ _ 1])
-apply (clarify, erule (3) 2)
-apply (clarify, rule 3)
-done
+  using 1 2 3 by (rule Bolzano)
 
 text{*We can always find a division that is fine wrt any gauge*}