removed generation of strange tuple modes in predicate compiler
authorbulwahn
Wed Sep 23 16:20:12 2009 +0200 (2009-09-23)
changeset 32666fd96d5f49d59
parent 32665 8bf46a97ff79
child 32667 09546e654222
removed generation of strange tuple modes in predicate compiler
src/HOL/ex/predicate_compile.ML
     1.1 --- a/src/HOL/ex/predicate_compile.ML	Wed Sep 23 16:20:12 2009 +0200
     1.2 +++ b/src/HOL/ex/predicate_compile.ML	Wed Sep 23 16:20:12 2009 +0200
     1.3 @@ -2119,7 +2119,7 @@
     1.4              case HOLogic.strip_tupleT U of
     1.5                [] => [(i + 1, NONE)]
     1.6              | [U] => [(i + 1, NONE)]
     1.7 -            | Us =>  map (pair (i + 1) o SOME) (subsets 1 (length Us)))
     1.8 +	    | Us =>  map (pair (i + 1) o SOME) ((subsets 1 (length Us)) \\ [[], 1 upto (length Us)]))
     1.9            Ts)
    1.10        in
    1.11          cprod (cprods (map (fn T => case strip_type T of