# HG changeset patch
# User bulwahn
# Date 1270046681 -7200
# Node ID 0c128c2c310d3735d2cd53076a57ae8a8d52d5c6
# Parent  537876d0fa6212eefd2f84d487fb01dd2b23594d
made smlnj happy

diff -r 537876d0fa62 -r 0c128c2c310d src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- 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 =