src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 40844 5895c525739d
parent 40139 6a53d57fa902
child 41228 e1fce873b814
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Dec 01 15:02:39 2010 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Dec 01 15:03:44 2010 +0100
     1.3 @@ -485,7 +485,7 @@
     1.4  
     1.5  fun is_pred thy constname = (body_type (Sign.the_const_type thy constname) = HOLogic.boolT);
     1.6  
     1.7 -fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = @{typ bool})
     1.8 +fun is_predT (T as Type("fun", [_, _])) = (body_type T = @{typ bool})
     1.9    | is_predT _ = false
    1.10  
    1.11  (*** check if a term contains only constructor functions ***)