src/HOL/Library/Predicate_Compile_Alternative_Defs.thy

   "A = B \<longleftrightarrow> (\<forall>x. A x \<longrightarrow> B x) \<and> (\<forall>x. B x \<longrightarrow> A x)"
   by (auto simp add: fun_eq_iff)
 
 section {* Setup for Numerals *}
 
-setup {* Predicate_Compile_Data.ignore_consts [@{const_name numeral}, @{const_name neg_numeral}] *}
-setup {* Predicate_Compile_Data.keep_functions [@{const_name numeral}, @{const_name neg_numeral}] *}
+setup {* Predicate_Compile_Data.ignore_consts [@{const_name numeral}] *}
+setup {* Predicate_Compile_Data.keep_functions [@{const_name numeral}] *}
 
 setup {* Predicate_Compile_Data.ignore_consts [@{const_name div}, @{const_name mod}, @{const_name times}] *}
 
 section {* Arithmetic operations *}