diff -r 99bf2b38d3ef -r 61faa204c810 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Tue May 31 17:05:44 2011 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Tue May 31 17:15:14 2011 +0200
@@ -271,8 +271,8 @@
  @{const_name "equal_bool_inst.equal_bool"},
  @{const_name "ord_fun_inst.less_eq_fun"},
  @{const_name "ord_fun_inst.less_fun"},
- @{const_name Metis.fequal},
  @{const_name Meson.skolem},
+ @{const_name ATP.fequal},
  @{const_name transfer_morphism},
  @{const_name enum_prod_inst.enum_all_prod},
  @{const_name enum_prod_inst.enum_ex_prod}