# HG changeset patch
# User wenzelm
# Date 975370153 -3600
# Node ID ced4f4ec917e9a8da104f704cc88221c5062f7a2
# Parent  3e21ab3e5114747236a42f4a4f161f0d78027ac6
consumes0/1;

diff -r 3e21ab3e5114 -r ced4f4ec917e src/HOL/Tools/induct_attrib.ML
--- a/src/HOL/Tools/induct_attrib.ML	Tue Nov 28 01:08:50 2000 +0100
+++ b/src/HOL/Tools/induct_attrib.ML	Tue Nov 28 01:09:13 2000 +0100
@@ -124,24 +124,28 @@
 
 local
 
-fun mk_att f g name (x, thm) = (f (g (name, thm)) x, thm);
+fun mk_att f g h name arg =
+  let val (x, thm) = h arg in (f (g (name, thm)) x, thm) end;
 
 fun add_casesT rule x = apfst (apfst (NetRules.insert rule)) x;
 fun add_casesS rule x = apfst (apsnd (NetRules.insert rule)) x;
 fun add_inductT rule x = apsnd (apfst (NetRules.insert rule)) x;
 fun add_inductS rule x = apsnd (apsnd (NetRules.insert rule)) x;
 
+fun consumes0 x = RuleCases.consumes_default 0 x;
+fun consumes1 x = RuleCases.consumes_default 1 x;
+
 in
 
-val cases_type_global = mk_att GlobalInduct.map add_casesT;
-val cases_set_global = mk_att GlobalInduct.map add_casesS;
-val induct_type_global = mk_att GlobalInduct.map add_inductT;
-val induct_set_global = mk_att GlobalInduct.map add_inductS;
+val cases_type_global = mk_att GlobalInduct.map add_casesT consumes0;
+val cases_set_global = mk_att GlobalInduct.map add_casesS consumes1;
+val induct_type_global = mk_att GlobalInduct.map add_inductT consumes0;
+val induct_set_global = mk_att GlobalInduct.map add_inductS consumes1;
 
-val cases_type_local = mk_att LocalInduct.map add_casesT;
-val cases_set_local = mk_att LocalInduct.map add_casesS;
-val induct_type_local = mk_att LocalInduct.map add_inductT;
-val induct_set_local = mk_att LocalInduct.map add_inductS;
+val cases_type_local = mk_att LocalInduct.map add_casesT consumes0;
+val cases_set_local = mk_att LocalInduct.map add_casesS consumes1;
+val induct_type_local = mk_att LocalInduct.map add_inductT consumes0;
+val induct_set_local = mk_att LocalInduct.map add_inductS consumes1;
 
 end;