diff -r 933d43c31689 -r defbcdc60fd6 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Jun 26 11:14:39 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Jun 26 11:14:39 2012 +0200
@@ -55,8 +55,7 @@
   val satallax_unsat_coreN : string
   val parse_formula :
     string list -> (string, 'a, (string, 'a) ho_term) formula * string list
-  val atp_proof_from_tstplike_proof :
-    string problem -> string -> string -> string proof
+  val atp_proof_from_tstplike_proof : string problem -> string -> string proof
   val clean_up_atp_proof_dependencies : string proof -> string proof
   val map_term_names_in_atp_proof :
     (string -> string) -> string proof -> string proof
@@ -485,8 +484,8 @@
                               (Scan.repeat1 (parse_line problem))))
        |> fst
 
-fun atp_proof_from_tstplike_proof _ _ "" = []
-  | atp_proof_from_tstplike_proof problem output tstp =
+fun atp_proof_from_tstplike_proof _ "" = []
+  | atp_proof_from_tstplike_proof problem tstp =
     tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
     |> parse_proof problem
     |> sort (step_name_ord o pairself step_name) (* FIXME: needed? *)