diff -r 0c4f18fe8218 -r f6532c597300 src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Mon Jan 23 14:07:36 2012 +0100 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Mon Jan 23 14:08:55 2012 +0100 @@ -258,6 +258,7 @@ ["HOL.induct_equal", "HOL.induct_implies", "HOL.induct_conj", + "HOL.induct_forall", @{const_name undefined}, @{const_name default}, @{const_name dummy_pattern}, @@ -276,7 +277,8 @@ @{const_name ATP.fequal}, @{const_name transfer_morphism}, @{const_name enum_prod_inst.enum_all_prod}, - @{const_name enum_prod_inst.enum_ex_prod} + @{const_name enum_prod_inst.enum_ex_prod}, + @{const_name Quickcheck.catch_match} (*@{const_name "==>"}, @{const_name "=="}*)] val forbidden_mutant_consts =