src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML

     Const (@{const_name Predicate.Pred}, T --> mk_predT T') $ f    
   end;
 
 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;
 
 fun dest_Eval (Const (@{const_name Predicate.eval}, _) $ f $ x) = (f, x)