1.1 --- a/src/Tools/induct.ML	Sun Nov 08 16:28:18 2009 +0100
     1.2 +++ b/src/Tools/induct.ML	Sun Nov 08 16:30:41 2009 +0100
     1.3 @@ -130,7 +130,7 @@
     1.4  
     1.5  (* context data *)
     1.6  
     1.7 -structure InductData = GenericDataFun
     1.8 +structure InductData = Generic_Data
     1.9  (
    1.10    type T = (rules * rules) * (rules * rules) * (rules * rules);
    1.11    val empty =
    1.12 @@ -138,7 +138,7 @@
    1.13       (init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
    1.14       (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)));
    1.15    val extend = I;
    1.16 -  fun merge _ (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1)),
    1.17 +  fun merge (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1)),
    1.18        ((casesT2, casesP2), (inductT2, inductP2), (coinductT2, coinductP2))) =
    1.19      ((Item_Net.merge (casesT1, casesT2), Item_Net.merge (casesP1, casesP2)),
    1.20        (Item_Net.merge (inductT1, inductT2), Item_Net.merge (inductP1, inductP2)),