# HG changeset patch
# User haftmann
# Date 1282209564 -7200
# Node ID 6c8806696bed2328bf7a360cb86b70bbb7151bb7
# Parent  8ddfc68a3908efb4ff30e907a0d6bd80907bf101
tuned

diff -r 8ddfc68a3908 -r 6c8806696bed src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Aug 19 11:19:24 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Aug 19 11:19:24 2010 +0200
@@ -429,10 +429,7 @@
   
 fun is_intro constname t = is_intro_term constname (prop_of t)
 
-fun is_pred thy constname =
-  let
-    val T = (Sign.the_const_type thy constname)
-  in body_type T = @{typ "bool"} end;
+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})
   | is_predT _ = false