--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Sun Feb 28 23:51:31 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Mon Mar 01 09:47:44 2010 +0100
@@ -22,7 +22,8 @@
structure Fun_Pred = Theory_Data
(
type T = (term * term) Item_Net.T;
- val empty = Item_Net.init (op aconv o pairself fst) (single o fst);
+ val empty = Item_Net.init ((op aconv o pairself fst) : (term * term) * (term * term) -> bool)
+ (single o fst);
val extend = I;
val merge = Item_Net.merge;
)