--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Aug 26 16:25:25 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Aug 26 16:34:10 2010 +0200
@@ -730,9 +730,7 @@
type T = (mode * (compilation_funs -> typ -> term)) list Symtab.table;
val empty = Symtab.empty;
val extend = I;
- val merge = Symtab.merge ((K true)
- : ((mode * (compilation_funs -> typ -> term)) list *
- (mode * (compilation_funs -> typ -> term)) list -> bool));
+ fun merge data : T = Symtab.merge (K true) data;
);
fun alternative_compilation_of_global thy pred_name mode =