| changeset 37591 | d3daea901123 |
| parent 36253 | 6e969ce3dfcc |
| child 39198 | f967a16dfcdd |
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Mon Jun 28 15:03:07 2010 +0200 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Mon Jun 28 15:03:07 2010 +0200 @@ -18,7 +18,7 @@ section {* Pairs *} -setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name split}] *} +setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name prod_case}] *} section {* Bounded quantifiers *}