diff -r 6f933b702f44 -r fde495b9e24b src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Wed Oct 05 10:56:06 2005 +0200
+++ b/src/HOL/Tools/res_clause.ML	Wed Oct 05 11:18:06 2005 +0200
@@ -32,7 +32,6 @@
   val isTaut : clause -> bool
   val num_of_clauses : clause -> int
 
-  val dfg_clauses2str : string list -> string
   val clause2dfg : clause -> string * string list
   val clauses2dfg : clause list -> string -> clause list -> clause list ->
 	   (string * int) list -> (string * int) list -> string
@@ -41,7 +40,6 @@
   val tptp_arity_clause : arityClause -> string
   val tptp_classrelClause : classrelClause -> string
   val tptp_clause : clause -> string list
-  val tptp_clauses2str : string list -> string
   val clause2tptp : clause -> string * string list
   val tfree_clause : string -> string
   val schematic_var_prefix : string
@@ -293,11 +291,11 @@
 	  val funcs' = ResLib.flat_noDup funcslist
 	  val t = make_fixed_type_const a
       in    
-	  ((t ^ paren_pack folTyps), (ts', (t, length Ts)::funcs') )
+	  ((t ^ paren_pack folTyps), (ts', (t, length Ts)::funcs'))
       end
   | type_of (TFree (a, s)) = 
       let val t = make_fixed_type_var a
-      in (t, ([((FOLTFree a),s)],[(t,0)]) ) end
+      in (t, ([((FOLTFree a),s)],[(t,0)])) end
   | type_of (TVar (v, s)) = (make_schematic_type_var v, ([((FOLTVar v),s)], []))
 
 
@@ -617,7 +615,7 @@
 	 val conclLit = make_TConsLit(true,(res,tcons,tvars))
          val tvars_srts = ListPair.zip (tvars,args)
 	 val tvars_srts' = ResLib.flat_noDup(map pack_sort tvars_srts)
-         val false_tvars_srts' = ResLib.pair_ins false tvars_srts'
+         val false_tvars_srts' = map (pair false) tvars_srts'
 	 val premLits = map make_TVarLit false_tvars_srts'
      in
 	 make_arity_clause (cls_id,Axiom,conclLit,premLits)
@@ -773,7 +771,7 @@
 |   uvar_name (Fun (a,_,_)) = raise CLAUSE("Not a variable", Const(a,dummyT));
 
 fun mergelist [] = []
-|   mergelist (x::xs ) = x @ mergelist xs
+|   mergelist (x::xs) = x @ mergelist xs
 
 fun dfg_vars (Clause cls) =
     let val lits = #literals cls
@@ -861,9 +859,6 @@
 
 fun string_of_end () = "end_problem.\n%------------------------------------------------------------------------------";
 
-val delim = "\n";
-val dfg_clauses2str = ResLib.list2str_sep delim; 
-     
 
 fun clause2dfg cls =
     let val (lits,tfree_lits) = dfg_clause_aux cls 
@@ -890,16 +885,16 @@
 fun gen_dfg_file probname axioms conjectures funcs preds = 
     let val axstrs_tfrees = (map clause2dfg axioms)
 	val (axstrs, atfrees) = ListPair.unzip axstrs_tfrees
-        val axstr = ResLib.list2str_sep delim axstrs
+        val axstr = (space_implode "\n" axstrs) ^ "\n\n"
         val conjstrs_tfrees = (map clause2dfg conjectures)
 	val (conjstrs, atfrees) = ListPair.unzip conjstrs_tfrees
         val tfree_clss = map tfree_dfg_clause (ResLib.flat_noDup atfrees) 
-        val conjstr = ResLib.list2str_sep delim (tfree_clss@conjstrs)
+        val conjstr = (space_implode "\n" (tfree_clss@conjstrs)) ^ "\n\n"
         val funcstr = string_of_funcs funcs
         val predstr = string_of_preds preds
     in
        (string_of_start probname) ^ (string_of_descrip ()) ^ 
-       (string_of_symbols funcstr predstr ) ^  
+       (string_of_symbols funcstr predstr) ^  
        (string_of_axioms axstr) ^
        (string_of_conjectures conjstr) ^ (string_of_end ())
     end;
@@ -1042,9 +1037,6 @@
 fun tfree_clause tfree_lit =
     "input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "]).";
 
-val delim = "\n";
-val tptp_clauses2str = ResLib.list2str_sep delim; 
-     
 
 fun tptp_of_arLit (TConsLit(b,(c,t,args))) =
       let val pol = if b then "++" else "--"