src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

 val encode_strs = map encode_str #> space_implode " "
 val unencode_str = String.explode #> unmeta_chars []
 val unencode_strs =
   space_explode " " #> filter_out (curry (op =) "") #> map unencode_str
 
-fun freshish_name () =
-  Date.fmt ".%Y%m%d_%H%M%S__" (Date.fromTimeLocal (Time.now ())) ^
-  serial_string ()
-
 (* Avoid scientific notation *)
 fun safe_str_of_real r =
   if r < 0.00001 then "0.00001"
   else if r >= 1000000.0 then "1000000"
   else Markup.print_real r

     ()
   end
 
 fun learn _ _ _ [] = ()
   | learn ctxt overlord save learns =
-    (trace_msg ctxt (fn () => "MaSh learn " ^
-         elide_string 1000 (space_implode " " (map #1 learns)));
-     run_mash_tool ctxt overlord ([] |> save ? cons save_models_arg) false
-                   (learns, str_of_learn) (K ()))
+    let val names = elide_string 1000 (space_implode " " (map #1 learns)) in
+      (trace_msg ctxt (fn () => "MaSh learn" ^ (if names = "" then "" else " " ^ names));
+       run_mash_tool ctxt overlord ([] |> save ? cons save_models_arg) false
+                     (learns, str_of_learn) (K ()))
+    end
 
 fun relearn _ _ _ [] = ()
   | relearn ctxt overlord save relearns =
     (trace_msg ctxt (fn () => "MaSh relearn " ^
          elide_string 1000 (space_implode " " (map #1 relearns)));

                      used_ths =
   if is_mash_enabled () then
     launch_thread (timeout |> the_default one_day) (fn () =>
         let
           val thy = Proof_Context.theory_of ctxt
-          val name = freshish_name ()
           val feats = features_of ctxt thy 0 Symtab.empty (Local, General) [t] |> map fst
         in
           peek_state ctxt overlord (fn {access_G, ...} =>
               let
                 val parents = maximal_wrt_access_graph access_G facts
                 val deps =
                   used_ths |> filter (is_fact_in_graph access_G)
                            |> map nickname_of_thm
               in
-                MaSh.learn ctxt overlord true [(name, parents, feats, deps)]
+                MaSh.learn ctxt overlord true [("", parents, feats, deps)]
               end);
           (true, "")
         end)
   else
     ()