# HG changeset patch
# User blanchet
# Date 1391090500 -3600
# Node ID 6e2295db4cf8edae59c5e02849e8b92ea0a0475e
# Parent  17ec4a29ef715585e6956079b6c5d58e05f856f7
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized

diff -r 17ec4a29ef71 -r 6e2295db4cf8 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Jan 30 14:37:53 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Jan 30 15:01:40 2014 +0100
@@ -95,17 +95,24 @@
 
 fun add_lines_pass3 res [] = rev res
   | add_lines_pass3 res ((name, role, t, rule, deps) :: lines) =
-    if role <> Plain orelse is_skolemize_rule rule orelse is_arith_rule rule orelse
-       is_datatype_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_lines_pass3 ((name, role, t, rule, deps) :: res) lines
-    else
-      add_lines_pass3 res (map (replace_dependencies_in_line (name, deps)) lines)
+    let
+      val is_last_line = null lines
+
+      fun looks_interesting () =
+        not (is_only_type_information t) andalso null (Term.add_tvars t [])
+        andalso length deps >= 2 andalso not (can the_single lines)
+
+      fun is_skolemizing_line (_, _, _, rule', deps') =
+        is_skolemize_rule rule' andalso member (op =) deps' name
+      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
+      else
+        add_lines_pass3 res (map (replace_dependencies_in_line (name, deps)) lines)
+    end
 
 val add_labels_of_proof =
   steps_of_proof