diff -r 6f8bbe9ca8a2 -r ce2297415b54 src/HOL/Mirabelle/Tools/mirabelle_metis.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Sat May 08 16:24:44 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Sat May 08 17:10:27 2010 +0200
@@ -13,7 +13,7 @@
 fun run id ({pre, post, timeout, log, ...}: Mirabelle.run_args) =
   let
     val thms = Mirabelle.theorems_of_sucessful_proof post
-    val names = map Thm.get_name thms
+    val names = map Thm.get_name_hint thms
     val add_info = if null names then I else suffix (":\n" ^ commas names)
 
     val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre))