# HG changeset patch
# User blanchet
# Date 1387135885 -3600
# Node ID b632390b5966d1c83df6a22cfceaedf66056478f
# Parent  ba488d89614a6456d5ac53a6e372a038f17ad0e7
tuning

diff -r ba488d89614a -r b632390b5966 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sun Dec 15 20:09:13 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sun Dec 15 20:31:25 2013 +0100
@@ -129,7 +129,7 @@
 fun is_only_type_information t = t aconv @{prop True}
 
 (* Discard facts; consolidate adjacent lines that prove the same formula, since they differ only in
-   type information.*)
+   type information. *)
 fun add_line_pass1 (line as (name as (_, ss), role, t, rule, [])) lines =
     (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire)
        internal facts or definitions. *)
@@ -211,7 +211,7 @@
         let
           val (l, subst, next) = (l, subst, next) |> fresh_label depth have_prefix
           val sub = relabel_proofs subst depth sub
-          val by = by |> relabel_byline subst
+          val by = apfst (relabel_facts subst) by
         in
           Prove (qs, xs, l, t, sub, by) :: relabel_steps subst depth next steps
         end
@@ -221,7 +221,6 @@
       let val (assms, subst) = relabel_assms subst depth assms in
         Proof (fix, assms, relabel_steps subst depth 1 steps)
       end
-    and relabel_byline subst byline = apfst (relabel_facts subst) byline
     and relabel_proofs subst depth = map (relabel_proof subst (depth + 1))
   in
     relabel_proof [] 0