src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML

   case resolve_conjecture ss of
     [j] => (conjecture_prefix, j)
   | _ => (raw_prefix ^ ascii_of num, 0)
 
 fun label_of_clause [name] = raw_label_for_name name
-  | label_of_clause c = (space_implode "___" (map fst c), 0)
+  | label_of_clause c = (space_implode "___" (map (fst o raw_label_for_name) c), 0)
 
 fun add_fact_from_dependencies fact_names (names as [(_, ss)]) =
     if is_fact fact_names ss then
       apsnd (union (op =) (map fst (resolve_fact fact_names ss)))
     else

         val (isar_proof, ext_time) =
           ref_graph
           |> redirect_graph axioms tainted
           |> map (do_inf true)
           |> append assms
-          (*|> relabel_proof (* FIXME: Is there a better way? *) *)
           |> (if not preplay andalso isar_shrink <= 1.0
               then pair (true, seconds 0.0) #> swap
               else shrink_proof debug ctxt type_enc lam_trans preplay
                 preplay_timeout (if isar_proofs then isar_shrink else 1000.0))
        (* |>> reorder_proof_to_minimize_jumps (* ? *) *)