src/HOL/Tools/ATP/atp_proof_reconstruct.ML

     val thy = Proof_Context.theory_of ctxt
     val var_index = var_index_of_textual true
 
     fun do_term opt_T u =
       (case u of
-        AAbs(((var, ty), term), []) =>
+        AAbs (((var, ty), term), []) =>
         let
           val typ = typ_of_atp_type ctxt ty
           val var_name = repair_var_name true var
           val tm = do_term NONE term
         in quantify_over_var true lambda' var_name typ tm end

     if member (op aconv) seen t then rev seen else take_distinct_vars (t :: seen) ts
   | take_distinct_vars seen _ = rev seen
 
 fun unskolemize_term skos t =
   let
-    val is_sko = member (op =) skos
+    val is_skolem = member (op =) skos
 
     fun find_args args (t $ u) = find_args (u :: args) t #> find_args [] u
       | find_args _ (Abs (_, _, t)) = find_args [] t
       | find_args args (Free (s, _)) =
-        if is_sko s then
+        if is_skolem s then
           let val new = take_distinct_vars [] args in
             (fn [] => new | old => if length new < length old then new else old)
           end
         else
           I

     val alls = find_args [] t []
     val num_alls = length alls
 
     fun fix_skos args (t $ u) = fix_skos (fix_skos [] u :: args) t
       | fix_skos args (t as Free (s, T)) =
-        if is_sko s then list_comb (Free (s, funpow num_alls body_type T), drop num_alls args)
+        if is_skolem s then list_comb (Free (s, funpow num_alls body_type T), drop num_alls args)
         else list_comb (t, args)
       | fix_skos [] (Abs (s, T, t)) = Abs (s, T, fix_skos [] t)
       | fix_skos [] t = t
       | fix_skos args t = list_comb (fix_skos [] t, args)
 
     val t' = fix_skos [] t
 
-    fun add_sko (t as Free (s, _)) = is_sko s ? insert (op aconv) t
-      | add_sko _ = I
-
-    val exs = Term.fold_aterms add_sko t' []
+    fun add_skolem (t as Free (s, _)) = is_skolem s ? insert (op aconv) t
+      | add_skolem _ = I
+
+    val exs = Term.fold_aterms add_skolem t' []
   in
     t'
     |> HOLogic.dest_Trueprop
     |> fold exists_of exs |> Term.map_abs_vars (K Name.uu)
     |> fold_rev forall_of alls
     |> HOLogic.mk_Trueprop
   end
 
+fun rename_skolem_args t =
+  let
+    fun add_skolem_args (Abs (_, _, t)) = add_skolem_args t
+      | add_skolem_args t =
+        (case strip_comb t of
+          (Free (s, _), args as _ :: _) =>
+          if String.isPrefix spass_skolem_prefix s then
+            insert (op =) (s, fst (take_prefix is_Var args))
+          else
+            fold add_skolem_args args
+        | (u, args as _ :: _) => fold add_skolem_args (u :: args)
+        | _ => I)
+
+    fun subst_of_skolem (sk, args) =
+      map_index (fn (j, Var (z, T)) => (z, Var ((sk ^ "_" ^ string_of_int j, 0), T))) args
+
+    val subst = maps subst_of_skolem (add_skolem_args t [])
+  in
+    subst_vars ([], subst) t
+  end
+
 fun introduce_spass_skolems proof =
   let
-    fun add_sko (Free (s, _)) = String.isPrefix spass_skolem_prefix s ? insert (op =) s
-      | add_sko _ = I
+    fun add_skolem (Free (s, _)) = String.isPrefix spass_skolem_prefix s ? insert (op =) s
+      | add_skolem _ = I
 
     (* union-find would be faster *)
     fun add_cycle [] = I
       | add_cycle ss =
         fold (fn s => Graph.default_node (s, ())) ss
         #> fold Graph.add_edge (ss ~~ tl ss @ [hd ss])
 
     val (input_steps, other_steps) = List.partition (null o #5) proof
 
-    val skoss = map (fn (_, _, t, _, _) => Term.fold_aterms add_sko t []) input_steps
+    val skoss = map (fn (_, _, t, _, _) => Term.fold_aterms add_skolem t []) input_steps
     val skoss_input_steps = filter_out (null o fst) (skoss ~~ input_steps)
     val groups = Graph.strong_conn (fold add_cycle skoss Graph.empty)
 
     fun step_name_of_group skos = (implode skos, [])
     fun in_group group = member (op =) group o hd

 
     fun new_steps (skoss_steps : (string list * (term, 'a) atp_step) list) group =
       let
         val name = step_name_of_group group
         val name0 = name |>> prefix "0"
-        val t = skoss_steps
-          |> map (snd #> #3 #> HOLogic.dest_Trueprop)
-          |> Library.foldr1 s_conj
-          |> HOLogic.mk_Trueprop
+        val t =
+          (case map (snd #> #3) skoss_steps of
+            [t] => t
+          | ts => ts
+            |> map (HOLogic.dest_Trueprop #> rename_skolem_args)
+            |> Library.foldr1 s_conj
+            |> HOLogic.mk_Trueprop)
         val skos = fold (union (op =) o fst) skoss_steps []
         val deps = map (snd #> #1) skoss_steps
       in
         [(name0, Unknown, unskolemize_term skos t, spass_pre_skolemize_rule, deps),
          (name, Unknown, t, spass_skolemize_rule, [name0])]