1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed May 19 18:24:03 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed May 19 18:24:04 2010 +0200
     1.3 @@ -3124,6 +3124,10 @@
     1.4                    instance_of (m1, Input) andalso instance_of (m2, Input)
     1.5                | instance_of (Pair (m1, m2), Output) =
     1.6                    instance_of (m1, Output) andalso instance_of (m2, Output)
     1.7 +              | instance_of (Input, Pair (m1, m2)) =
     1.8 +                  instance_of (Input, m1) andalso instance_of (Input, m2)
     1.9 +              | instance_of (Output, Pair (m1, m2)) =
    1.10 +                  instance_of (Output, m1) andalso instance_of (Output, m2)
    1.11                | instance_of _ = false
    1.12            in forall instance_of (strip_fun_mode m1 ~~ strip_fun_mode m2) end
    1.13          val derivs = all_derivations_of thy (all_modes_of thy) [] body