# HG changeset patch
# User wenzelm
# Date 1223991945 -7200
# Node ID d6f60fcb1b772ef864b36c8cb1109473ede0193f
# Parent  581b2ab9827a2a5feec18906f5d5f40a3aeae1e2
tuned;

diff -r 581b2ab9827a -r d6f60fcb1b77 src/HOL/Tools/atp_thread.ML
--- a/src/HOL/Tools/atp_thread.ML	Tue Oct 14 15:45:44 2008 +0200
+++ b/src/HOL/Tools/atp_thread.ML	Tue Oct 14 15:45:45 2008 +0200
@@ -12,10 +12,10 @@
   val problem_name: string ref
   (* basic template *)
   val external_prover:
-    ((int -> Path.T) -> Proof.context * Thm.thm list * Thm.thm -> string list * ResHolClause.axiom_name Vector.vector list) ->
+    ((int -> Path.T) -> Proof.context * thm list * thm -> string list * ResHolClause.axiom_name Vector.vector list) ->
     Path.T * string ->
     (string * int -> bool) ->
-    (string * string vector * Proof.context * Thm.thm * int -> string) ->
+    (string * string vector * Proof.context * thm * int -> string) ->
     int -> Proof.state -> Thread.thread
   (* provers as functions returning threads *)
   val tptp_prover_filter_opts_full: int -> bool -> bool -> Path.T * string -> int -> Proof.state -> Thread.thread
@@ -55,7 +55,7 @@
       let val probfile = Path.basic (problem_name' ^ serial_string () ^ "_" ^ Int.toString nr)
       in if destdir' = "" then File.tmp_path probfile
         else if File.exists (Path.explode (destdir'))
-        then (Path.append  (Path.explode (destdir')) probfile)
+        then Path.append  (Path.explode (destdir')) probfile
         else error ("No such directory: " ^ destdir')
       end
     (* write out problem file and call prover *)