# HG changeset patch
# User hoelzl
# Date 1428920129 -7200
# Node ID cd2b6debac181cac0b05a282dfb327d0f6fc8f1c
# Parent  7c4a2e87e4d0596b1d206ac5338da5fa49b123d0
predicate compiler: ignore Abs_filter and Rep_filter

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]