# HG changeset patch
# User blanchet
# Date 1412615956 -7200
# Node ID 85fa90262807312d77e9e49933fdeb2c8780b11a
# Parent  c9e8ad426ab1a634d92627ecb0cbc9044205451e
avoid creating needless skolemization steps for SPASS

diff -r c9e8ad426ab1 -r 85fa90262807 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Oct 06 19:19:16 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Oct 06 19:19:16 2014 +0200
@@ -721,14 +721,16 @@
     (* The names of the formulas are added to the Skolem constants, to ensure that formulas giving
        rise to several clauses are skolemized together. *)
     val skoXss = map (fn ((_, ss), _, t, _, _) => Term.fold_aterms add_skolem t ss) input_steps
-    val skoXss_input_steps = filter_out (null o fst) (skoXss ~~ input_steps)
-    val groups = Graph.strong_conn (fold add_cycle skoXss Graph.empty)
+    val groups0 = Graph.strong_conn (fold add_cycle skoXss Graph.empty)
+    val groups = filter (exists (String.isPrefix spass_skolem_prefix)) groups0
+
+    val skoXss_input_steps = skoXss ~~ input_steps
 
     fun step_name_of_group skoXs = (implode skoXs, [])
     fun in_group group = member (op =) group o hd
-    fun group_of skoX = the (find_first (fn group => in_group group skoX) groups)
+    fun group_of skoX = find_first (fn group => in_group group skoX) groups
 
-    fun new_steps (skoXss_steps : (string list * (term, 'a) atp_step) list) group =
+    fun new_steps skoXss_steps group =
       let
         val name = step_name_of_group group
         val name0 = name |>> prefix "0"
@@ -751,7 +753,8 @@
       maps (fn group => new_steps (filter (in_group group o fst) skoXss_input_steps) group) groups
 
     val old_news =
-      map (fn (skos, (name, _, _, _, _)) => (name, [step_name_of_group (group_of skos)]))
+      map_filter (fn (skoXs, (name, _, _, _, _)) =>
+          Option.map (pair name o single o step_name_of_group) (group_of skoXs))
         skoXss_input_steps
     val repair_deps = fold replace_dependencies_in_line old_news
   in