--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Mar 31 16:44:41 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Mar 31 16:44:41 2010 +0200
@@ -717,7 +717,9 @@
type T = (mode * (compilation_funs -> typ -> term)) list Symtab.table;
val empty = Symtab.empty;
val extend = I;
- val merge = Symtab.merge (K true);
+ val merge = Symtab.merge ((K true)
+ : ((mode * (compilation_funs -> typ -> term)) list *
+ (mode * (compilation_funs -> typ -> term)) list -> bool));
);
fun alternative_compilation_of thy pred_name mode =