use structure File instead of TextIO;
removed comments

--- a/src/HOL/Tools/atp_wrapper.ML	Sun Jun 28 15:01:28 2009 +0200
+++ b/src/HOL/Tools/atp_wrapper.ML	Sun Jun 28 15:01:28 2009 +0200
@@ -75,20 +75,16 @@
 
     (* write out problem file and call prover *)
     val probfile = prob_pathname subgoalno
-    val fname = File.platform_path probfile
-    val _ = writer fname clauses
-    val cmdline =
-      if File.exists cmd then "exec " ^ File.shell_path cmd ^ " " ^ args
-      else error ("Bad executable: " ^ Path.implode cmd)
-    val (proof, rc) = system_out (cmdline ^ " " ^ fname)
+    val _ = writer probfile clauses
+    val (proof, rc) = system_out (
+      if File.exists cmd then
+        space_implode " " ["exec", File.shell_path cmd, args, File.platform_path probfile]
+      else error ("Bad executable: " ^ Path.implode cmd))
 
     (* if problemfile has not been exported, delete problemfile; otherwise export proof, too *)
     val _ =
-      if destdir' = "" then OS.FileSys.remove fname
-      else
-        let val out = TextIO.openOut (fname ^ "_proof")
-        val _ = TextIO.output (out, proof)
-        in TextIO.closeOut out end
+      if destdir' = "" then File.rm probfile
+      else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof
     
     (* check for success and print out some information on failure *)
     val failure = find_failure proof

--- a/src/HOL/Tools/res_clause.ML	Sun Jun 28 15:01:28 2009 +0200
+++ b/src/HOL/Tools/res_clause.ML	Sun Jun 28 15:01:28 2009 +0200
@@ -57,7 +57,6 @@
   val add_foltype_funcs: fol_type * int Symtab.table -> int Symtab.table
   val add_arityClause_funcs: arityClause * int Symtab.table -> int Symtab.table
   val init_functab: int Symtab.table
-  val writeln_strs: TextIO.outstream -> string list -> unit
   val dfg_sign: bool -> string -> string
   val dfg_of_typeLit: bool -> type_literal -> string
   val gen_dfg_cls: int * string * kind * string list * string list * string list -> string
@@ -441,8 +440,6 @@
 fun string_of_type_clsname (cls_id,ax_name,idx) =
     string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx);
 
-fun writeln_strs os = List.app (fn s => TextIO.output (os, s));
-
 
 (**** Producing DFG files ****)
 

--- a/src/HOL/Tools/res_hol_clause.ML	Sun Jun 28 15:01:28 2009 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML	Sun Jun 28 15:01:28 2009 +0200
@@ -26,18 +26,18 @@
   val strip_comb: combterm -> combterm * combterm list
   val literals_of_term: theory -> term -> literal list * typ list
   exception TOO_TRIVIAL
-  val make_conjecture_clauses:  bool -> theory -> thm list -> clause list (* dfg thy ccls *)
+  val make_conjecture_clauses:  bool -> theory -> thm list -> clause list
   val make_axiom_clauses: bool ->
        theory ->
-       (thm * (axiom_name * clause_id)) list -> (axiom_name * clause) list (* dfg thy axcls *)
+       (thm * (axiom_name * clause_id)) list -> (axiom_name * clause) list
   val get_helper_clauses: bool ->
        theory ->
        bool ->
        clause list * (thm * (axiom_name * clause_id)) list * string list ->
        clause list
-  val tptp_write_file: bool -> string ->
+  val tptp_write_file: bool -> Path.T ->
     clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit
-  val dfg_write_file: bool -> string -> 
+  val dfg_write_file: bool -> Path.T ->
     clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit
 end
 
@@ -469,59 +469,56 @@
 
 (* tptp format *)
 
-fun tptp_write_file t_full filename clauses =
+fun tptp_write_file t_full file clauses =
   let
     val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses
     val (cma, cnh) = count_constants clauses
     val params = (t_full, cma, cnh)
     val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
     val tfree_clss = map RC.tptp_tfree_clause (List.foldl (op union_string) [] tfree_litss)
-    val out = TextIO.openOut filename
   in
-    List.app (curry TextIO.output out o #1 o (clause2tptp params)) axclauses;
-    RC.writeln_strs out tfree_clss;
-    RC.writeln_strs out tptp_clss;
-    List.app (curry TextIO.output out o RC.tptp_classrelClause) classrel_clauses;
-    List.app (curry TextIO.output out o RC.tptp_arity_clause) arity_clauses;
-    List.app (curry TextIO.output out o #1 o (clause2tptp params)) helper_clauses;
-    TextIO.closeOut out
+    File.write_list file (
+      map (#1 o (clause2tptp params)) axclauses @
+      tfree_clss @
+      tptp_clss @
+      map RC.tptp_classrelClause classrel_clauses @
+      map RC.tptp_arity_clause arity_clauses @
+      map (#1 o (clause2tptp params)) helper_clauses)
   end;
 
 
 (* dfg format *)
 
-fun dfg_write_file t_full filename clauses =
+fun dfg_write_file t_full file clauses =
   let
     val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses
     val (cma, cnh) = count_constants clauses
     val params = (t_full, cma, cnh)
     val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures)
-    and probname = Path.implode (Path.base (Path.explode filename))
+    and probname = Path.implode (Path.base file)
     val axstrs = map (#1 o (clause2dfg params)) axclauses
     val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss)
-    val out = TextIO.openOut filename
     val helper_clauses_strs = map (#1 o (clause2dfg params)) helper_clauses
     val (funcs,cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
     and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
   in
-    TextIO.output (out, RC.string_of_start probname);
-    TextIO.output (out, RC.string_of_descrip probname);
-    TextIO.output (out, RC.string_of_symbols
-                          (RC.string_of_funcs funcs)
-                          (RC.string_of_preds (cl_preds @ ty_preds)));
-    TextIO.output (out, "list_of_clauses(axioms,cnf).\n");
-    RC.writeln_strs out axstrs;
-    List.app (curry TextIO.output out o RC.dfg_classrelClause) classrel_clauses;
-    List.app (curry TextIO.output out o RC.dfg_arity_clause) arity_clauses;
-    RC.writeln_strs out helper_clauses_strs;
-    TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n");
-    RC.writeln_strs out tfree_clss;
-    RC.writeln_strs out dfg_clss;
-    TextIO.output (out, "end_of_list.\n\n");
-    (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
-    TextIO.output (out, "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n");
-    TextIO.output (out, "end_problem.\n");
-    TextIO.closeOut out
+    File.write_list file (
+      RC.string_of_start probname ::
+      RC.string_of_descrip probname ::
+      RC.string_of_symbols (RC.string_of_funcs funcs)
+        (RC.string_of_preds (cl_preds @ ty_preds)) ::
+      "list_of_clauses(axioms,cnf).\n" ::
+      axstrs @
+      map RC.dfg_classrelClause classrel_clauses @
+      map RC.dfg_arity_clause arity_clauses @
+      helper_clauses_strs @
+      ["end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"] @
+      tfree_clss @
+      dfg_clss @
+      ["end_of_list.\n\n",
+      (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
+       "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n",
+       "end_problem.\n"])
   end;
 
 end