src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Oct 20 20:03:23 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Oct 20 20:54:31 2009 +0200
@@ -615,7 +615,7 @@
 fun guess_nparams T =
   let
     val argTs = binder_types T
-    val nparams = fold (curry Int.max)
+    val nparams = fold Integer.max
       (map (fn x => x + 1) (find_indexes is_predT argTs)) 0
   in nparams end;