diff -r f380fbd6e329 -r 674df68d4df0 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Sun Nov 01 20:55:39 2009 +0100
+++ b/src/HOL/Tools/Function/function_common.ML	Sun Nov 01 20:59:34 2009 +0100
@@ -92,9 +92,7 @@
 structure FunctionData = GenericDataFun
 (
   type T = (term * function_context_data) Item_Net.T;
-  val empty = Item_Net.init
-    (op aconv o pairself fst : (term * function_context_data) * (term * function_context_data) -> bool)
-    fst;
+  val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
   val copy = I;
   val extend = I;
   fun merge _ (tab1, tab2) = Item_Net.merge (tab1, tab2)
@@ -138,7 +136,7 @@
 val all_function_data = Item_Net.content o get_function
 
 fun add_function_data (data as FunctionCtxData {fs, termination, ...}) =
-    FunctionData.map (fold (fn f => Item_Net.insert (f, data)) fs)
+    FunctionData.map (fold (fn f => Item_Net.update (f, data)) fs)
     #> store_termination_rule termination