1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sun Dec 15 20:09:13 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sun Dec 15 20:31:25 2013 +0100
     1.3 @@ -129,7 +129,7 @@
     1.4  fun is_only_type_information t = t aconv @{prop True}
     1.5  
     1.6  (* Discard facts; consolidate adjacent lines that prove the same formula, since they differ only in
     1.7 -   type information.*)
     1.8 +   type information. *)
     1.9  fun add_line_pass1 (line as (name as (_, ss), role, t, rule, [])) lines =
    1.10      (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire)
    1.11         internal facts or definitions. *)
    1.12 @@ -211,7 +211,7 @@
    1.13          let
    1.14            val (l, subst, next) = (l, subst, next) |> fresh_label depth have_prefix
    1.15            val sub = relabel_proofs subst depth sub
    1.16 -          val by = by |> relabel_byline subst
    1.17 +          val by = apfst (relabel_facts subst) by
    1.18          in
    1.19            Prove (qs, xs, l, t, sub, by) :: relabel_steps subst depth next steps
    1.20          end
    1.21 @@ -221,7 +221,6 @@
    1.22        let val (assms, subst) = relabel_assms subst depth assms in
    1.23          Proof (fix, assms, relabel_steps subst depth 1 steps)
    1.24        end
    1.25 -    and relabel_byline subst byline = apfst (relabel_facts subst) byline
    1.26      and relabel_proofs subst depth = map (relabel_proof subst (depth + 1))
    1.27    in
    1.28      relabel_proof [] 0