# HG changeset patch
# User blanchet
# Date 1391103428 -3600
# Node ID f127ab7368cfe8ba8c18b7c3fb45d8e4ed7b9d4a
# Parent  fafdf2424c57abdc2dadad8ca4362632e030c6c9
killed needless pass

diff -r fafdf2424c57 -r f127ab7368cf src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Jan 30 17:34:42 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Jan 30 18:37:08 2014 +0100
@@ -85,16 +85,8 @@
       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
 
@@ -109,9 +101,9 @@
       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 =
@@ -237,8 +229,7 @@
         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, _, _, _) =>