src/Tools/induct.ML
changeset 45375 7fe19930dfc9
parent 45328 e5b33eecbf6e
child 46961 5c6955f487e5
     1.1 --- a/src/Tools/induct.ML	Sun Nov 06 21:17:45 2011 +0100
     1.2 +++ b/src/Tools/induct.ML	Sun Nov 06 21:51:46 2011 +0100
     1.3 @@ -290,8 +290,12 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun mk_att f g name arg =
     1.8 -  let val (x, thm) = g arg in (Data.map (f (name, thm)) x, thm) end;
     1.9 +fun mk_att f g name =
    1.10 +  Thm.mixed_attribute (fn (context, thm) =>
    1.11 +    let
    1.12 +      val thm' = g thm;
    1.13 +      val context' = Data.map (f (name, thm')) context;
    1.14 +    in (context', thm') end);
    1.15  
    1.16  fun del_att which =
    1.17    Thm.declaration_attribute (fn th => Data.map (which (pairself (fn rs =>
    1.18 @@ -309,8 +313,8 @@
    1.19  fun add_coinductT rule x = map3 (apfst (Item_Net.update rule)) x;
    1.20  fun add_coinductP rule x = map3 (apsnd (Item_Net.update rule)) x;
    1.21  
    1.22 -val consumes0 = Rule_Cases.consumes_default 0;
    1.23 -val consumes1 = Rule_Cases.consumes_default 1;
    1.24 +val consumes0 = Rule_Cases.default_consumes 0;
    1.25 +val consumes1 = Rule_Cases.default_consumes 1;
    1.26  
    1.27  in
    1.28