# HG changeset patch
# User blanchet
# Date 1285320988 -7200
# Node ID fabd6b48fe6e887e94b2068f908c90a492724061
# Parent  a89040dd6416b460e3cb1909e2e80b7c3792ac15# Parent  6fcd95367c67150b7be9831e030a58be8648c6a2
merge

diff -r a89040dd6416 -r fabd6b48fe6e src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Sep 24 10:27:11 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Sep 24 11:36:28 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