Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed generation of strange tuple modes in predicate compiler
authorbulwahn
Wed, 23 Sep 2009 16:20:12 +0200
changeset 32666 fd96d5f49d59
parent 32665 8bf46a97ff79
child 32667 09546e654222
removed generation of strange tuple modes in predicate compiler
src/HOL/ex/predicate_compile.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle