diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/ex/Gauge_Integration.thy
--- a/src/HOL/ex/Gauge_Integration.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/ex/Gauge_Integration.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -45,7 +45,7 @@
       \<Longrightarrow> fine \<delta> (a, c) ((a, x, b) # D)"
 
 lemmas fine_induct [induct set: fine] =
-  fine.induct [of "\<delta>" "(a,b)" "D" "split P", unfolded split_conv, standard]
+  fine.induct [of "\<delta>" "(a,b)" "D" "split P", unfolded split_conv] for \<delta> a b D P
 
 lemma fine_single:
   "\<lbrakk>a < b; a \<le> x; x \<le> b; b - a < \<delta> x\<rbrakk> \<Longrightarrow> fine \<delta> (a, b) [(a, x, b)]"