# HG changeset patch
# User haftmann
# Date 1244120444 -7200
# Node ID ee1d5bec4ce3ea4fcc3b5c35294421e09769f902
# Parent  c02b3fd764f474a5843e50db96b0f670eea72f8a
made SML/NJ happy

diff -r c02b3fd764f4 -r ee1d5bec4ce3 src/HOL/ex/predicate_compile.ML
--- a/src/HOL/ex/predicate_compile.ML	Thu Jun 04 13:26:51 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Thu Jun 04 15:00:44 2009 +0200
@@ -143,7 +143,7 @@
                nparams = Symtab.empty};
   val copy = I;
   val extend = I;
-  fun merge _ r = {names = PredModetab.merge (op =) (pairself #names r),
+  fun merge _ (r : T * T) = {names = PredModetab.merge (op =) (pairself #names r),
                    modes = Symtab.merge (op =) (pairself #modes r),
                    function_defs = Symtab.merge Thm.eq_thm (pairself #function_defs r),
                    function_intros = Symtab.merge Thm.eq_thm (pairself #function_intros r),