# HG changeset patch
# User bulwahn
# Date 1303308046 -7200
# Node ID c3d880b13aa9eb6386775760d8fcdfca8950be1a
# Parent  1914fd5d7c0ea0986c0e9fbb3cc148a0126e7951
adding two further code-generator internal constants to the blacklist of Mutabelle

diff -r 1914fd5d7c0e -r c3d880b13aa9 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Apr 20 16:00:45 2011 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Apr 20 16:00:46 2011 +0200
@@ -273,7 +273,9 @@
  @{const_name "ord_fun_inst.less_fun"},
  @{const_name Metis.fequal},
  @{const_name Meson.skolem},
- @{const_name transfer_morphism}
+ @{const_name transfer_morphism},
+ @{const_name enum_prod_inst.enum_all_prod},
+ @{const_name enum_prod_inst.enum_ex_prod}
  (*@{const_name "==>"}, @{const_name "=="}*)]
 
 val forbidden_mutant_consts =