diff -r 170f4cc34697 -r 9191942c4ead src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Tue Nov 13 11:00:29 2007 +0100
+++ b/src/HOL/Transitive_Closure.thy	Tue Nov 13 11:02:55 2007 +0100
@@ -97,7 +97,7 @@
   thus ?thesis by iprover
 qed
 
-lemmas rtrancl_induct [consumes 1, induct set: rtrancl] = rtranclp_induct [to_set]
+lemmas rtrancl_induct [induct set: rtrancl] = rtranclp_induct [to_set]
 
 lemmas rtranclp_induct2 =
   rtranclp_induct[of _ "(ax,ay)" "(bx,by)", split_rule,
@@ -241,7 +241,7 @@
     by induct (iprover intro: cases dest!: conversepD rtranclp_converseD)+
 qed
 
-lemmas converse_rtrancl_induct[consumes 1] = converse_rtranclp_induct [to_set]
+lemmas converse_rtrancl_induct = converse_rtranclp_induct [to_set]
 
 lemmas converse_rtranclp_induct2 =
   converse_rtranclp_induct[of _ "(ax,ay)" "(bx,by)", split_rule,
@@ -324,7 +324,7 @@
   thus ?thesis by iprover
 qed
 
-lemmas trancl_induct [consumes 1, induct set: trancl] = tranclp_induct [to_set]
+lemmas trancl_induct [induct set: trancl] = tranclp_induct [to_set]
 
 lemmas tranclp_induct2 =
   tranclp_induct[of _ "(ax,ay)" "(bx,by)", split_rule,