src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML

       lines |> is_only_type_information t ? map (replace_dependencies_in_line (name, []))
     else
       map (replace_dependencies_in_line (name, [])) lines
   | add_line_pass1 line lines = line :: lines
 
-(* Recursively delete empty lines (type information) from the proof.
-   (FIXME: needed? And why is "delete_dependency" so complicated?) *)
-fun add_line_pass2 (line as (name, _, t, _, [])) lines =
-    if is_only_type_information t then delete_dependency name lines else line :: lines
-  | add_line_pass2 line lines = line :: lines
-and delete_dependency name lines =
-  fold_rev add_line_pass2 (map (replace_dependencies_in_line (name, [])) lines) []
-
-fun add_lines_pass3 res [] = rev res
-  | add_lines_pass3 res ((name, role, t, rule, deps) :: lines) =
+fun add_lines_pass2 res [] = rev res
+  | add_lines_pass2 res ((name, role, t, rule, deps) :: lines) =
     let
       val is_last_line = null lines
 
       fun looks_interesting () =
         not (is_only_type_information t) andalso null (Term.add_tvars t [])

       fun is_before_skolemize_rule () = exists is_skolemizing_line lines
     in
       if role <> Plain orelse is_skolemize_rule rule orelse is_arith_rule rule orelse
          is_datatype_rule rule orelse is_last_line orelse looks_interesting () orelse
          is_before_skolemize_rule () then
-        add_lines_pass3 ((name, role, t, rule, deps) :: res) lines
+        add_lines_pass2 ((name, role, t, rule, deps) :: res) lines
       else
-        add_lines_pass3 res (map (replace_dependencies_in_line (name, deps)) lines)
+        add_lines_pass2 res (map (replace_dependencies_in_line (name, deps)) lines)
     end
 
 val add_labels_of_proof =
   steps_of_proof
   #> fold_isar_steps (byline_of_step #> (fn SOME ((ls, _), _) => union (op =) ls | _ => I))

           if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE
 
         val atp_proof =
           atp_proof
           |> rpair [] |-> fold_rev add_line_pass1
-          |> rpair [] |-> fold_rev add_line_pass2
-          |> add_lines_pass3 []
+          |> add_lines_pass2 []
 
         val conjs =
           map_filter (fn (name, role, _, _, _) =>
               if member (op =) [Conjecture, Negated_Conjecture] role then SOME name else NONE)
             atp_proof