diff -r 6f8bbe9ca8a2 -r ce2297415b54 src/HOL/Mutabelle/mutabelle.ML
--- a/src/HOL/Mutabelle/mutabelle.ML	Sat May 08 16:24:44 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle.ML	Sat May 08 17:10:27 2010 +0200
@@ -648,7 +648,7 @@
        val mutated = mutate option (prop_of x) usedthy
          commutatives forbidden_funs iter
        val (passednum,_,cenum,_) = qc_test mutated insts usedthy sz qciter
-       val thmname =  "\ntheorem " ^ (Thm.get_name x) ^ ":"
+       val thmname =  "\ntheorem " ^ Thm.get_name_hint x ^ ":"
        val pnumstring = string_of_int passednum
        val cenumstring = string_of_int cenum
      in