# HG changeset patch
# User bulwahn
# Date 1327328553 -3600
# Node ID 40522961d4b11df5beb33dd1bf263daeeabd52d3
# Parent  f6532c5973007c94e943a1a3fc596aa65deae769
adding another internal constant to mutabelle's blacklust

diff -r f6532c597300 -r 40522961d4b1 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Jan 23 14:08:55 2012 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Jan 23 15:22:33 2012 +0100
@@ -278,7 +278,8 @@
  @{const_name transfer_morphism},
  @{const_name enum_prod_inst.enum_all_prod},
  @{const_name enum_prod_inst.enum_ex_prod},
- @{const_name Quickcheck.catch_match}
+ @{const_name Quickcheck.catch_match},
+ @{const_name Quickcheck_Exhaustive.unknown}
  (*@{const_name "==>"}, @{const_name "=="}*)]
 
 val forbidden_mutant_consts =