# HG changeset patch
# User bulwahn
# Date 1253715612 -7200
# Node ID fd96d5f49d59dfca317c4c772c8959743ef1bae5
# Parent  8bf46a97ff7994f6747dba37d0bfacd9786c313b
removed generation of strange tuple modes in predicate compiler

diff -r 8bf46a97ff79 -r fd96d5f49d59 src/HOL/ex/predicate_compile.ML
--- a/src/HOL/ex/predicate_compile.ML	Wed Sep 23 16:20:12 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Wed Sep 23 16:20:12 2009 +0200
@@ -2119,7 +2119,7 @@
             case HOLogic.strip_tupleT U of
               [] => [(i + 1, NONE)]
             | [U] => [(i + 1, NONE)]
-            | Us =>  map (pair (i + 1) o SOME) (subsets 1 (length Us)))
+	    | Us =>  map (pair (i + 1) o SOME) ((subsets 1 (length Us)) \\ [[], 1 upto (length Us)]))
           Ts)
       in
         cprod (cprods (map (fn T => case strip_type T of