--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Thu Aug 26 16:25:25 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Thu Aug 26 16:34:10 2010 +0200
@@ -18,8 +18,7 @@
structure Specialisations = Theory_Data
(
type T = (term * term) Item_Net.T;
- val empty = Item_Net.init ((op aconv o pairself fst) : (term * term) * (term * term) -> bool)
- (single o fst);
+ val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
val extend = I;
val merge = Item_Net.merge;
)