diff -r 24563731b9b2 -r e31a85f92ce9 src/Pure/Tools/named_thms.ML
--- 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;