# HG changeset patch
# User blanchet
# Date 1328353698 -3600
# Node ID 4ed12518fb8148090b4124a011b0f80f8336d74d
# Parent  505465fae291bb8750f07663f042582195c286f5
improved hashing w.r.t. Mirabelle, to help debugging

diff -r 505465fae291 -r 4ed12518fb81 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Sat Feb 04 12:08:18 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Sat Feb 04 12:08:18 2012 +0100
@@ -684,6 +684,20 @@
    is still necessary). *)
 val reserved_nice_names = [tptp_old_equal, "op", "eq"]
 
+(* hack to get the same hashing across Mirabelle runs (see "mirabelle.pl") *)
+fun cleanup_mirabelle_name s =
+  let
+    val mirabelle_infix = "_Mirabelle_"
+    val random_suffix_len = 10
+    val (s1, s2) = Substring.position mirabelle_infix (Substring.full s)
+  in
+    if Substring.isEmpty s2 then
+      s
+    else
+      Substring.string s1 ^
+      Substring.string (Substring.triml (size mirabelle_infix + random_suffix_len) s2)
+  end
+
 fun readable_name protect full_name s =
   (if s = full_name then
      s
@@ -694,7 +708,7 @@
        |> (fn s =>
               if size s > max_readable_name_size then
                 String.substring (s, 0, max_readable_name_size div 2 - 4) ^
-                string_of_int (hash_string full_name) ^
+                string_of_int (hash_string (cleanup_mirabelle_name full_name)) ^
                 String.extract (s, size s - max_readable_name_size div 2 + 4,
                                 NONE)
               else