--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Dec 01 15:02:39 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Dec 01 15:03:44 2010 +0100
@@ -485,7 +485,7 @@
fun is_pred thy constname = (body_type (Sign.the_const_type thy constname) = HOLogic.boolT);
-fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = @{typ bool})
+fun is_predT (T as Type("fun", [_, _])) = (body_type T = @{typ bool})
| is_predT _ = false
(*** check if a term contains only constructor functions ***)