--- 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