diff -r ea7d0df15be0 -r b1b21a8f6362 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 29 17:30:53 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 29 17:30:54 2010 +0200
@@ -1940,7 +1940,8 @@
         (case alternative_function_of (ProofContext.theory_of ctxt) name mode of
           SOME alt_function_name =>
             let
-              val (inpTs, outpTs) = split_modeT' mode (binder_types T)
+              val (inpTs, outpTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE))
+                mode (binder_types T)
               val bs = map (pair "x") inpTs
               val bounds = map Bound (rev (0 upto (length bs) - 1))
               val f = Const (alt_function_name, inpTs ---> HOLogic.mk_tupleT outpTs)