| changeset 55414 | eab03e9cee8a |
| parent 54489 | 03ff4d1e6784 |
| child 56073 | 29e308b56d23 |
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Wed Feb 12 08:35:56 2014 +0100 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Wed Feb 12 08:35:57 2014 +0100 @@ -22,7 +22,7 @@ section {* Pairs *} -setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name prod_case}] *} +setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name case_prod}] *} section {* Bounded quantifiers *}