src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Thu Sep 23 10:39:25 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Thu Sep 23 14:50:13 2010 +0200
@@ -47,7 +47,7 @@
 
 fun mk_Eval (f, x) =
   let
-    val T = fastype_of x
+    val T = dest_predT (fastype_of f)
   in
     Const (@{const_name Predicate.eval}, mk_predT T --> T --> HOLogic.boolT) $ f $ x
   end;