src/Tools/induct.ML
changeset 33373 674df68d4df0
parent 33368 b1cf34f1855c
child 33519 e31a85f92ce9
     1.1 --- a/src/Tools/induct.ML	Sun Nov 01 20:55:39 2009 +0100
     1.2 +++ b/src/Tools/induct.ML	Sun Nov 01 20:59:34 2009 +0100
     1.3 @@ -113,9 +113,10 @@
     1.4  
     1.5  type rules = (string * thm) Item_Net.T;
     1.6  
     1.7 -val init_rules =
     1.8 -  Item_Net.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso
     1.9 -    Thm.eq_thm_prop (th1, th2));
    1.10 +fun init_rules index : rules =
    1.11 +  Item_Net.init
    1.12 +    (fn ((s1, th1), (s2, th2)) => s1 = s2 andalso Thm.eq_thm_prop (th1, th2))
    1.13 +    (single o index);
    1.14  
    1.15  fun filter_rules (rs: rules) th =
    1.16    filter (fn (_, th') => Thm.eq_thm_prop (th, th')) (Item_Net.content rs);
    1.17 @@ -203,18 +204,18 @@
    1.18    let val (x, thm) = g arg in (InductData.map (f (name, thm)) x, thm) end;
    1.19  
    1.20  fun del_att which = Thm.declaration_attribute (fn th => InductData.map (which (pairself (fn rs =>
    1.21 -  fold Item_Net.delete (filter_rules rs th) rs))));
    1.22 +  fold Item_Net.remove (filter_rules rs th) rs))));
    1.23  
    1.24  fun map1 f (x, y, z) = (f x, y, z);
    1.25  fun map2 f (x, y, z) = (x, f y, z);
    1.26  fun map3 f (x, y, z) = (x, y, f z);
    1.27  
    1.28 -fun add_casesT rule x = map1 (apfst (Item_Net.insert rule)) x;
    1.29 -fun add_casesP rule x = map1 (apsnd (Item_Net.insert rule)) x;
    1.30 -fun add_inductT rule x = map2 (apfst (Item_Net.insert rule)) x;
    1.31 -fun add_inductP rule x = map2 (apsnd (Item_Net.insert rule)) x;
    1.32 -fun add_coinductT rule x = map3 (apfst (Item_Net.insert rule)) x;
    1.33 -fun add_coinductP rule x = map3 (apsnd (Item_Net.insert rule)) x;
    1.34 +fun add_casesT rule x = map1 (apfst (Item_Net.update rule)) x;
    1.35 +fun add_casesP rule x = map1 (apsnd (Item_Net.update rule)) x;
    1.36 +fun add_inductT rule x = map2 (apfst (Item_Net.update rule)) x;
    1.37 +fun add_inductP rule x = map2 (apsnd (Item_Net.update rule)) x;
    1.38 +fun add_coinductT rule x = map3 (apfst (Item_Net.update rule)) x;
    1.39 +fun add_coinductP rule x = map3 (apsnd (Item_Net.update rule)) x;
    1.40  
    1.41  val consumes0 = Rule_Cases.consumes_default 0;
    1.42  val consumes1 = Rule_Cases.consumes_default 1;