src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 38552 6c8806696bed
parent 38549 d0385f2764d8
child 38558 32ad17fe2b9c
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Aug 19 11:19:24 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Aug 19 11:19:24 2010 +0200
     1.3 @@ -429,10 +429,7 @@
     1.4    
     1.5  fun is_intro constname t = is_intro_term constname (prop_of t)
     1.6  
     1.7 -fun is_pred thy constname =
     1.8 -  let
     1.9 -    val T = (Sign.the_const_type thy constname)
    1.10 -  in body_type T = @{typ "bool"} end;
    1.11 +fun is_pred thy constname = (body_type (Sign.the_const_type thy constname) = HOLogic.boolT);
    1.12  
    1.13  fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = @{typ bool})
    1.14    | is_predT _ = false