src/HOL/Tools/inductive_set.ML
changeset 33519 e31a85f92ce9
parent 33459 a4a38ed813f7
child 33643 b275f26a638b
     1.1 --- a/src/HOL/Tools/inductive_set.ML	Sun Nov 08 16:28:18 2009 +0100
     1.2 +++ b/src/HOL/Tools/inductive_set.ML	Sun Nov 08 16:30:41 2009 +0100
     1.3 @@ -152,7 +152,7 @@
     1.4  (* where s and p are parameters                            *)
     1.5  (***********************************************************)
     1.6  
     1.7 -structure PredSetConvData = GenericDataFun
     1.8 +structure PredSetConvData = Generic_Data
     1.9  (
    1.10    type T =
    1.11      {(* rules for converting predicates to sets *)
    1.12 @@ -166,7 +166,7 @@
    1.13    val empty = {to_set_simps = [], to_pred_simps = [],
    1.14      set_arities = Symtab.empty, pred_arities = Symtab.empty};
    1.15    val extend = I;
    1.16 -  fun merge _
    1.17 +  fun merge
    1.18      ({to_set_simps = to_set_simps1, to_pred_simps = to_pred_simps1,
    1.19        set_arities = set_arities1, pred_arities = pred_arities1},
    1.20       {to_set_simps = to_set_simps2, to_pred_simps = to_pred_simps2,