# 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