# HG changeset patch
# User bulwahn
# Date 1274286244 -7200
# Node ID 34e73e8bab6623c42b5ac14d665d0aa6752ac4c1
# Parent  bcffdb8991674fda319e152cfc6f80c467bbdf70
improved values command to handle a special case with tuples and polymorphic predicates more correctly

diff -r bcffdb899167 -r 34e73e8bab66 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed May 19 18:24:03 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed May 19 18:24:04 2010 +0200
@@ -3124,6 +3124,10 @@
                   instance_of (m1, Input) andalso instance_of (m2, Input)
               | instance_of (Pair (m1, m2), Output) =
                   instance_of (m1, Output) andalso instance_of (m2, Output)
+              | instance_of (Input, Pair (m1, m2)) =
+                  instance_of (Input, m1) andalso instance_of (Input, m2)
+              | instance_of (Output, Pair (m1, m2)) =
+                  instance_of (Output, m1) andalso instance_of (Output, m2)
               | instance_of _ = false
           in forall instance_of (strip_fun_mode m1 ~~ strip_fun_mode m2) end
         val derivs = all_derivations_of thy (all_modes_of thy) [] body