src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML

 
 (* No "real" literals means only type information (tfree_tcs, clsrel, or clsarity). *)
 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. *)
     if role = Lemma orelse role = Conjecture orelse role = Negated_Conjecture orelse
        role = Hypothesis orelse is_arith_rule rule then

     fun relabel_steps _ _ _ [] = []
       | relabel_steps subst depth next (Prove (qs, xs, l, t, sub, by) :: steps) =
         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
       | relabel_steps subst depth next (step :: steps) =
         step :: relabel_steps subst depth next steps
     and relabel_proof subst depth (Proof (fix, assms, steps)) =
       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
   end