src/HOL/Tools/res_atp_setup.ML

 fun atp_axioms_g tptp_ax_fn rules file =
     let val out = TextIO.openOut file
 	val (clss,errs) = tptp_ax_fn rules
 	val clss' = ResClause.union_all clss
     in
-	ResAtp.writeln_strs out clss';
+	ResClause.writeln_strs out clss';
 	TextIO.closeOut out;
 	([file],errs)
     end;
 
 

     end;
 
 fun atp_conjectures_h_g filt_conj_fn hyp_cls =
     let val (tptp_h_clss,tfree_litss) = filt_conj_fn hyp_cls
 	val tfree_lits = ResClause.union_all tfree_litss
-	val tfree_clss = map ResClause.tfree_clause tfree_lits 
+	val tfree_clss = map ResClause.tptp_tfree_clause tfree_lits 
 	val hypsfile = hyps_file ()
         val out = TextIO.openOut(hypsfile)
     in
-        ResAtp.writeln_strs out (tfree_clss @ tptp_h_clss);
+        ResClause.writeln_strs out (tfree_clss @ tptp_h_clss);
         TextIO.closeOut out; warning hypsfile;
         ([hypsfile],tfree_lits)
     end;
 
 fun atp_conjectures_h_fol hyp_cls = atp_conjectures_h_g filtered_tptp_conjectures_fol hyp_cls;
 
 fun atp_conjectures_h_hol hyp_cls = atp_conjectures_h_g filtered_tptp_conjectures_hol hyp_cls;
 
 fun atp_conjectures_c_g filt_conj_fn conj_cls n tfrees =
     let val (tptp_c_clss,tfree_litss) = filt_conj_fn conj_cls
-	val tfree_clss = map ResClause.tfree_clause ((ResClause.union_all tfree_litss) \\ tfrees)
+	val tfree_clss = map ResClause.tptp_tfree_clause ((ResClause.union_all tfree_litss) \\ tfrees)
 	val probfile = prob_file n
 	val out = TextIO.openOut(probfile)		 	
     in
-	ResAtp.writeln_strs out (tfree_clss @ tptp_c_clss);
+	ResClause.writeln_strs out (tfree_clss @ tptp_c_clss);
 	TextIO.closeOut out;
 	warning probfile; 
 	probfile 
     end;
 

 	val arity_cls = map ResClause.tptp_arity_clause arity_clauses
 	fun write_ts () =
 	    let val tsfile = types_sorts_file ()
 		val out = TextIO.openOut(tsfile)
 	    in
-		ResAtp.writeln_strs out (classrel_cls @ arity_cls);
+		ResClause.writeln_strs out (classrel_cls @ arity_cls);
 		TextIO.closeOut out;
 		[tsfile]
 	    end
     in
 	if (List.null arity_cls andalso List.null classrel_cls) then []