diff -r 7c4a2e87e4d0 -r cd2b6debac18 src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Apr 13 12:13:52 2015 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Apr 13 12:15:29 2015 +0200
@@ -24,6 +24,11 @@
 
 setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name case_prod}] *}
 
+section {* Filters *}
+
+(*TODO: shouldn't this be done by typedef? *)
+setup {* Predicate_Compile_Data.ignore_consts [@{const_name Abs_filter}, @{const_name Rep_filter}] *}
+
 section {* Bounded quantifiers *}
 
 declare Ball_def[code_pred_inline]