diff -r 24563731b9b2 -r e31a85f92ce9 src/HOL/Tools/Function/context_tree.ML
--- a/src/HOL/Tools/Function/context_tree.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/HOL/Tools/Function/context_tree.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -44,12 +44,12 @@
 open Function_Common
 open Function_Lib
 
-structure FunctionCongs = GenericDataFun
+structure FunctionCongs = Generic_Data
 (
   type T = thm list
   val empty = []
   val extend = I
-  fun merge _ = Thm.merge_thms
+  val merge = Thm.merge_thms
 );
 
 val get_function_congs = FunctionCongs.get o Context.Proof