--- 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]