reverse order in which lines are selected, to ensure that the number of dependencies is accurate

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Dec 11 22:23:42 2013 +0800
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Dec 11 22:53:32 2013 +0800
@@ -109,19 +109,19 @@
 
 val is_skolemize_rule = member (op =) [e_skolemize_rule, vampire_skolemisation_rule]
 
-fun add_desired_line (name as (_, ss), role, t, rule, deps) (j, lines) =
-  (j + 1,
-   if role <> Plain orelse is_skolemize_rule rule orelse
-      (* the last line must be kept *)
-      j = 0 orelse
-      (not (is_only_type_information t) andalso
-       null (Term.add_tvars t []) andalso
-       length deps >= 2 andalso
-       (* kill next to last line, which usually results in a trivial step *)
-       j <> 1) then
-     (name, role, t, rule, deps) :: lines  (* keep line *)
-   else
-     map (replace_dependencies_in_line (name, deps)) lines)  (* drop line *)
+fun add_desired_lines res [] = rev res
+  | add_desired_lines res ((name as (_, ss), role, t, rule, deps) :: lines) =
+    if role <> Plain orelse is_skolemize_rule rule orelse
+       (* the last line must be kept *)
+       null lines orelse
+       (not (is_only_type_information t) andalso
+        null (Term.add_tvars t []) andalso
+        length deps >= 2 andalso
+        (* don't keep next to last line, which usually results in a trivial step *)
+        not (can the_single lines)) then
+      add_desired_lines ((name, role, t, rule, deps) :: res) lines
+    else
+      add_desired_lines res (map (replace_dependencies_in_line (name, deps)) lines)
 
 val add_labels_of_proof =
   steps_of_proof
@@ -235,9 +235,7 @@
           |> truncate_at_false
           |> rpair [] |-> fold_rev add_line
           |> rpair [] |-> fold_rev add_nontrivial_line
-          |> rpair (0, [])
-          |-> fold_rev add_desired_line
-          |> snd
+          |> add_desired_lines []
 
         val conjs =
           map_filter (fn (name, role, _, _, _) =>