# HG changeset patch
# User bulwahn
# Date 1285308730 -7200
# Node ID 632bcdb80d8858e739bab85d23c5478cdd8a02e2
# Parent  9d554d257a1075107d4fb0d6ad87a671e1db1daf
being a little less strict than in 2e06dad03dd3

diff -r 9d554d257a10 -r 632bcdb80d88 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Sep 23 21:17:11 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Sep 24 08:12:10 2010 +0200
@@ -431,7 +431,8 @@
 fun check_matches_type ctxt predname T ms =
   let
     fun check (m as Fun (m1, m2)) (Type("fun", [T1,T2])) = check m1 T1 andalso check m2 T2
-      | check m (Type("fun", _)) = false
+      | check m (T as Type("fun", _)) =
+        if body_type T = @{typ bool} then false else (m = Input orelse m = Output)
       | check (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) =
           check m1 T1 andalso check m2 T2 
       | check Input T = true