1.1 --- a/src/HOL/Tools/res_clause.ML	Wed Oct 05 10:56:06 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Wed Oct 05 11:18:06 2005 +0200
     1.3 @@ -32,7 +32,6 @@
     1.4    val isTaut : clause -> bool
     1.5    val num_of_clauses : clause -> int
     1.6  
     1.7 -  val dfg_clauses2str : string list -> string
     1.8    val clause2dfg : clause -> string * string list
     1.9    val clauses2dfg : clause list -> string -> clause list -> clause list ->
    1.10  	   (string * int) list -> (string * int) list -> string
    1.11 @@ -41,7 +40,6 @@
    1.12    val tptp_arity_clause : arityClause -> string
    1.13    val tptp_classrelClause : classrelClause -> string
    1.14    val tptp_clause : clause -> string list
    1.15 -  val tptp_clauses2str : string list -> string
    1.16    val clause2tptp : clause -> string * string list
    1.17    val tfree_clause : string -> string
    1.18    val schematic_var_prefix : string
    1.19 @@ -293,11 +291,11 @@
    1.20  	  val funcs' = ResLib.flat_noDup funcslist
    1.21  	  val t = make_fixed_type_const a
    1.22        in    
    1.23 -	  ((t ^ paren_pack folTyps), (ts', (t, length Ts)::funcs') )
    1.24 +	  ((t ^ paren_pack folTyps), (ts', (t, length Ts)::funcs'))
    1.25        end
    1.26    | type_of (TFree (a, s)) = 
    1.27        let val t = make_fixed_type_var a
    1.28 -      in (t, ([((FOLTFree a),s)],[(t,0)]) ) end
    1.29 +      in (t, ([((FOLTFree a),s)],[(t,0)])) end
    1.30    | type_of (TVar (v, s)) = (make_schematic_type_var v, ([((FOLTVar v),s)], []))
    1.31  
    1.32  
    1.33 @@ -617,7 +615,7 @@
    1.34  	 val conclLit = make_TConsLit(true,(res,tcons,tvars))
    1.35           val tvars_srts = ListPair.zip (tvars,args)
    1.36  	 val tvars_srts' = ResLib.flat_noDup(map pack_sort tvars_srts)
    1.37 -         val false_tvars_srts' = ResLib.pair_ins false tvars_srts'
    1.38 +         val false_tvars_srts' = map (pair false) tvars_srts'
    1.39  	 val premLits = map make_TVarLit false_tvars_srts'
    1.40       in
    1.41  	 make_arity_clause (cls_id,Axiom,conclLit,premLits)
    1.42 @@ -773,7 +771,7 @@
    1.43  |   uvar_name (Fun (a,_,_)) = raise CLAUSE("Not a variable", Const(a,dummyT));
    1.44  
    1.45  fun mergelist [] = []
    1.46 -|   mergelist (x::xs ) = x @ mergelist xs
    1.47 +|   mergelist (x::xs) = x @ mergelist xs
    1.48  
    1.49  fun dfg_vars (Clause cls) =
    1.50      let val lits = #literals cls
    1.51 @@ -861,9 +859,6 @@
    1.52  
    1.53  fun string_of_end () = "end_problem.\n%------------------------------------------------------------------------------";
    1.54  
    1.55 -val delim = "\n";
    1.56 -val dfg_clauses2str = ResLib.list2str_sep delim; 
    1.57 -     
    1.58  
    1.59  fun clause2dfg cls =
    1.60      let val (lits,tfree_lits) = dfg_clause_aux cls 
    1.61 @@ -890,16 +885,16 @@
    1.62  fun gen_dfg_file probname axioms conjectures funcs preds = 
    1.63      let val axstrs_tfrees = (map clause2dfg axioms)
    1.64  	val (axstrs, atfrees) = ListPair.unzip axstrs_tfrees
    1.65 -        val axstr = ResLib.list2str_sep delim axstrs
    1.66 +        val axstr = (space_implode "\n" axstrs) ^ "\n\n"
    1.67          val conjstrs_tfrees = (map clause2dfg conjectures)
    1.68  	val (conjstrs, atfrees) = ListPair.unzip conjstrs_tfrees
    1.69          val tfree_clss = map tfree_dfg_clause (ResLib.flat_noDup atfrees) 
    1.70 -        val conjstr = ResLib.list2str_sep delim (tfree_clss@conjstrs)
    1.71 +        val conjstr = (space_implode "\n" (tfree_clss@conjstrs)) ^ "\n\n"
    1.72          val funcstr = string_of_funcs funcs
    1.73          val predstr = string_of_preds preds
    1.74      in
    1.75         (string_of_start probname) ^ (string_of_descrip ()) ^ 
    1.76 -       (string_of_symbols funcstr predstr ) ^  
    1.77 +       (string_of_symbols funcstr predstr) ^  
    1.78         (string_of_axioms axstr) ^
    1.79         (string_of_conjectures conjstr) ^ (string_of_end ())
    1.80      end;
    1.81 @@ -1042,9 +1037,6 @@
    1.82  fun tfree_clause tfree_lit =
    1.83      "input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "]).";
    1.84  
    1.85 -val delim = "\n";
    1.86 -val tptp_clauses2str = ResLib.list2str_sep delim; 
    1.87 -     
    1.88  
    1.89  fun tptp_of_arLit (TConsLit(b,(c,t,args))) =
    1.90        let val pol = if b then "++" else "--"