Removed some case_names and consumes attributes that are now no longer
needed due to changes in the to_pred and to_set attributes.

--- 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,

--- a/src/HOL/Wellfounded_Recursion.thy	Tue Nov 13 11:00:29 2007 +0100
+++ b/src/HOL/Wellfounded_Recursion.thy	Tue Nov 13 11:02:55 2007 +0100
@@ -71,8 +71,7 @@
 
 lemmas wf_induct_rule = wf_induct [rule_format, consumes 1, case_names less, induct set: wf]
 
-lemmas wfP_induct_rule =
-  wf_induct_rule [to_pred, consumes 1, case_names less, induct set: wfP]
+lemmas wfP_induct_rule = wf_induct_rule [to_pred, induct set: wfP]
 
 lemma wf_not_sym [rule_format]: "wf(r) ==> ALL x. (a,x):r --> (x,a)~:r"
 by (erule_tac a=a in wf_induct, blast)