# HG changeset patch
# User smolkas
# Date 1354101943 -3600
# Node ID 6dc80eead659d470c33f5268e8126a10400dfcc6
# Parent  a1a1685b4ee842c68347ab7c17429f897ae78dab
fixed problem with fact names

diff -r a1a1685b4ee8 -r 6dc80eead659 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Nov 28 12:25:06 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Nov 28 12:25:43 2012 +0100
@@ -293,7 +293,7 @@
   | _ => (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
@@ -709,7 +709,6 @@
           |> 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