--- 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),