--- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri Aug 27 19:34:23 2010 +0200
@@ -202,7 +202,7 @@
(@{const_name "top_fun_inst.top_fun"}, "'a"),
(@{const_name "Pure.term"}, "'a"),
(@{const_name "top_class.top"}, "'a"),
- (@{const_name "eq_class.eq"}, "'a"),
+ (@{const_name "HOL.equal"}, "'a"),
(@{const_name "Quotient.Quot_True"}, "'a")(*,
(@{const_name "uminus"}, "'a"),
(@{const_name "Nat.size"}, "'a"),
@@ -237,7 +237,7 @@
@{const_name "top_fun_inst.top_fun"},
@{const_name "Pure.term"},
@{const_name "top_class.top"},
- @{const_name "eq_class.eq"},
+ @{const_name "HOL.equal"},
@{const_name "Quotient.Quot_True"}]
fun is_forbidden_mutant t =