# HG changeset patch
# User bulwahn
# Date 1327324135 -3600
# Node ID f6532c5973007c94e943a1a3fc596aa65deae769
# Parent  0c4f18fe8218e7489c99b768bf0485d64409b776
adding some more forbidden constant names for the mutated conjecture generation

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 =