# HG changeset patch
# User bulwahn
# Date 1327392749 -3600
# Node ID 9a5d8e7684e552d164ffa987b3e974baa1d0385a
# Parent  b170ab46513a0f2a4414529e19a1edb5eeb77b4d
some more constants on mutabelle's blacklist

diff -r b170ab46513a -r 9a5d8e7684e5 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Jan 23 17:40:32 2012 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Jan 24 09:12:29 2012 +0100
@@ -275,6 +275,7 @@
  @{const_name "ord_fun_inst.less_fun"},
  @{const_name Meson.skolem},
  @{const_name ATP.fequal},
+ @{const_name ATP.fEx},
  @{const_name transfer_morphism},
  @{const_name enum_prod_inst.enum_all_prod},
  @{const_name enum_prod_inst.enum_ex_prod},
@@ -301,7 +302,8 @@
    (@{const_name "GCD.gcd_class.lcm"}, @{typ "prop => prop => prop"}),
    (@{const_name "Orderings.bot_class.bot"}, @{typ "bool => prop"}),
    (@{const_name "Groups.one_class.one"}, @{typ "bool => prop"}),
-   (@{const_name "Groups.zero_class.zero"},@{typ "bool => prop"})]
+   (@{const_name "Groups.zero_class.zero"},@{typ "bool => prop"}),
+   (@{const_name "equal_class.equal"},@{typ "bool => bool => bool"})]
 
 fun is_forbidden_mutant t =
   let