src/Pure/Tools/named_thms.ML
changeset 33519 e31a85f92ce9
parent 33453 fe551dc9d4bd
child 36296 5cc547abd995
     1.1 --- a/src/Pure/Tools/named_thms.ML	Sun Nov 08 16:28:18 2009 +0100
     1.2 +++ b/src/Pure/Tools/named_thms.ML	Sun Nov 08 16:30:41 2009 +0100
     1.3 @@ -17,12 +17,12 @@
     1.4  functor Named_Thms(val name: string val description: string): NAMED_THMS =
     1.5  struct
     1.6  
     1.7 -structure Data = GenericDataFun
     1.8 +structure Data = Generic_Data
     1.9  (
    1.10    type T = thm Item_Net.T;
    1.11    val empty = Thm.full_rules;
    1.12    val extend = I;
    1.13 -  fun merge _ = Item_Net.merge;
    1.14 +  val merge = Item_Net.merge;
    1.15  );
    1.16  
    1.17  val content = Item_Net.content o Data.get;