diff -r a8e96847523c -r eab03e9cee8a src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
--- 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 *}