--- a/src/HOL/Tools/function_package/fundef_common.ML Fri Apr 20 17:58:25 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML Fri Apr 20 17:58:26 2007 +0200
@@ -82,7 +82,9 @@
val name = "HOL/function_def/data";
type T = (term * fundef_context_data) NetRules.T
- val empty = NetRules.init (op aconv o pairself fst) fst;
+ val empty = NetRules.init
+ (op aconv o pairself fst : (term * fundef_context_data) * (term * fundef_context_data) -> bool)
+ fst;
val copy = I;
val extend = I;
fun merge _ (tab1, tab2) = NetRules.merge (tab1, tab2)