clarified rule structure;

--- a/src/HOL/Hilbert_Choice.thy	Mon Mar 21 20:38:39 2016 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Mon Mar 21 21:18:08 2016 +0100
@@ -762,7 +762,7 @@
   next
     fix n m :: nat assume "m < n" "n \<le> N"
     then show "f m < f n"
-    proof (induct rule: less_Suc_induct[consumes 1])
+    proof (induct rule: less_Suc_induct)
       case (1 i)
       then have "i < N" by simp
       then have "f i \<noteq> f (Suc i)"

--- a/src/HOL/Nat.thy	Mon Mar 21 20:38:39 2016 +0100
+++ b/src/HOL/Nat.thy	Mon Mar 21 21:18:08 2016 +0100
@@ -928,7 +928,7 @@
   by (rule less_induct) (auto intro: step simp:le_simps)
 
 text\<open>An induction rule for estabilishing binary relations\<close>
-lemma less_Suc_induct:
+lemma less_Suc_induct [consumes 1]:
   assumes less:  "i < j"
      and  step:  "!!i. P i (Suc i)"
      and  trans: "!!i j k. i < j ==> j < k ==>  P i j ==> P j k ==> P i k"
@@ -1646,7 +1646,7 @@
 proof (cases "n < n'")
   case True
   then show ?thesis
-    by (induct n n' rule: less_Suc_induct [consumes 1]) (auto intro: mono)
+    by (induct n n' rule: less_Suc_induct) (auto intro: mono)
 qed (insert \<open>n \<le> n'\<close>, auto) \<comment> \<open>trivial for @{prop "n = n'"}\<close>
 
 lemma lift_Suc_antimono_le:
@@ -1655,14 +1655,14 @@
 proof (cases "n < n'")
   case True
   then show ?thesis
-    by (induct n n' rule: less_Suc_induct [consumes 1]) (auto intro: mono)
+    by (induct n n' rule: less_Suc_induct) (auto intro: mono)
 qed (insert \<open>n \<le> n'\<close>, auto) \<comment> \<open>trivial for @{prop "n = n'"}\<close>
 
 lemma lift_Suc_mono_less:
   assumes mono: "\<And>n. f n < f (Suc n)" and "n < n'"
   shows "f n < f n'"
 using \<open>n < n'\<close>
-by (induct n n' rule: less_Suc_induct [consumes 1]) (auto intro: mono)
+by (induct n n' rule: less_Suc_induct) (auto intro: mono)
 
 lemma lift_Suc_mono_less_iff:
   "(\<And>n. f n < f (Suc n)) \<Longrightarrow> f n < f m \<longleftrightarrow> n < m"