# HG changeset patch
# User wenzelm
# Date 1135207719 -3600
# Node ID c0794cdbc6d1f3087b4426ce9359826b5bc5b651
# Parent  356a9f7118996b405071185dc22b69e411220ca9
wf_induct_rule: consumes 1;

diff -r 356a9f711899 -r c0794cdbc6d1 src/HOL/Wellfounded_Recursion.thy
--- a/src/HOL/Wellfounded_Recursion.thy	Thu Dec 22 00:28:36 2005 +0100
+++ b/src/HOL/Wellfounded_Recursion.thy	Thu Dec 22 00:28:39 2005 +0100
@@ -56,7 +56,7 @@
      |]  ==>  P(a)"
 by (unfold wf_def, blast)
 
-lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]
+lemmas wf_induct_rule = wf_induct [rule_format, consumes 1, case_names less, induct set: wf]
 
 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)