# HG changeset patch
# User wenzelm
# Date 1273331427 -7200
# Node ID ce2297415b5461acfec1317e5d3b457a9d379d86
# Parent  6f8bbe9ca8a295f66532b33c59d92ea48a35e556
prefer Thm.get_name_hint, which is closer to a user-space idea of "theorem name";

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))
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
diff -r 6f8bbe9ca8a2 -r ce2297415b54 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Sat May 08 16:24:44 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Sat May 08 17:10:27 2010 +0200
@@ -302,7 +302,7 @@
   end
 
 fun create_entry thy thm exec mutants mtds =
-  (Thm.get_name thm, exec, map (test_mutants_using_one_method thy mutants) mtds)
+  (Thm.get_name_hint thm, exec, map (test_mutants_using_one_method thy mutants) mtds)
 *)
 fun create_detailed_entry thy thm exec mutants mtds =
   let
@@ -310,7 +310,7 @@
       map (fn (mtd_name, invoke_mtd) =>
         (mtd_name, safe_invoke_mtd thy (mtd_name, invoke_mtd) mutant)) mtds)
   in
-    (Thm.get_name thm, exec, prop_of thm, map create_mutant_subentry mutants)
+    (Thm.get_name_hint thm, exec, prop_of thm, map create_mutant_subentry mutants)
   end
 
 (* (theory -> thm -> bool -> term list -> mtd list -> 'a) -> theory -> mtd list -> thm -> 'a *)