--- a/src/Tools/induct.ML Sun Nov 06 21:17:45 2011 +0100
+++ b/src/Tools/induct.ML Sun Nov 06 21:51:46 2011 +0100
@@ -290,8 +290,12 @@
local
-fun mk_att f g name arg =
- let val (x, thm) = g arg in (Data.map (f (name, thm)) x, thm) end;
+fun mk_att f g name =
+ Thm.mixed_attribute (fn (context, thm) =>
+ let
+ val thm' = g thm;
+ val context' = Data.map (f (name, thm')) context;
+ in (context', thm') end);
fun del_att which =
Thm.declaration_attribute (fn th => Data.map (which (pairself (fn rs =>
@@ -309,8 +313,8 @@
fun add_coinductT rule x = map3 (apfst (Item_Net.update rule)) x;
fun add_coinductP rule x = map3 (apsnd (Item_Net.update rule)) x;
-val consumes0 = Rule_Cases.consumes_default 0;
-val consumes1 = Rule_Cases.consumes_default 1;
+val consumes0 = Rule_Cases.default_consumes 0;
+val consumes1 = Rule_Cases.default_consumes 1;
in