changeset 33519 | e31a85f92ce9 |
parent 33453 | fe551dc9d4bd |
child 36296 | 5cc547abd995 |
--- a/src/Pure/Tools/named_thms.ML Sun Nov 08 16:28:18 2009 +0100 +++ b/src/Pure/Tools/named_thms.ML Sun Nov 08 16:30:41 2009 +0100 @@ -17,12 +17,12 @@ functor Named_Thms(val name: string val description: string): NAMED_THMS = struct -structure Data = GenericDataFun +structure Data = Generic_Data ( type T = thm Item_Net.T; val empty = Thm.full_rules; val extend = I; - fun merge _ = Item_Net.merge; + val merge = Item_Net.merge; ); val content = Item_Net.content o Data.get;