--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Oct 25 21:17:13 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Oct 25 21:17:14 2010 +0200
@@ -319,7 +319,7 @@
fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
let
val [depth] = additional_arguments
- val (_, Ts) = split_modeT' mode (binder_types T)
+ val (_, Ts) = split_modeT mode (binder_types T)
val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts)
val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
in