diff -r 7d46aa03696e -r 087d81f5213e src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Apr 06 22:11:01 2015 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Apr 06 23:14:05 2015 +0200
@@ -247,10 +247,10 @@
   end
 
 val forbidden_mutant_constnames =
- ["HOL.induct_equal",
-  "HOL.induct_implies",
-  "HOL.induct_conj",
-  "HOL.induct_forall",
+[@{const_name HOL.induct_equal},
+ @{const_name HOL.induct_implies},
+ @{const_name HOL.induct_conj},
+ @{const_name HOL.induct_forall},
  @{const_name undefined},
  @{const_name default},
  @{const_name Pure.dummy_pattern},