1.1 --- a/src/HOL/Tools/res_clause.ML	Thu Sep 15 17:45:17 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Thu Sep 15 17:46:00 2005 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4    val dfg_clauses2str : string list -> string
     1.5    val clause2dfg : clause -> string * string list
     1.6    val clauses2dfg : clause list -> string -> clause list -> clause list ->
     1.7 -	   (string * int) list -> (string * int) list -> string list -> string
     1.8 +	   (string * int) list -> (string * int) list -> string
     1.9    val tfree_dfg_clause : string -> string
    1.10  
    1.11    val tptp_arity_clause : arityClause -> string
    1.12 @@ -878,16 +878,16 @@
    1.13  
    1.14  
    1.15  fun tfree_dfg_clause tfree_lit =
    1.16 -  "clause( %(conjecture)\n" ^ "or( " ^ tfree_lit ^ ")),\n" ^ "tfree_tcs" ^ ")."
    1.17 +  "clause( %(conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ")."
    1.18  
    1.19  
    1.20 -fun gen_dfg_file probname axioms conjectures funcs preds tfrees= 
    1.21 +fun gen_dfg_file probname axioms conjectures funcs preds = 
    1.22      let val axstrs_tfrees = (map clause2dfg axioms)
    1.23  	val (axstrs, atfrees) = ListPair.unzip axstrs_tfrees
    1.24          val axstr = ResLib.list2str_sep delim axstrs
    1.25          val conjstrs_tfrees = (map clause2dfg conjectures)
    1.26  	val (conjstrs, atfrees) = ListPair.unzip conjstrs_tfrees
    1.27 -        val tfree_clss = map tfree_dfg_clause ((ResLib.flat_noDup atfrees) \\ tfrees) 
    1.28 +        val tfree_clss = map tfree_dfg_clause (ResLib.flat_noDup atfrees) 
    1.29          val conjstr = ResLib.list2str_sep delim (tfree_clss@conjstrs)
    1.30          val funcstr = string_of_funcs funcs
    1.31          val predstr = string_of_preds preds
    1.32 @@ -898,14 +898,13 @@
    1.33         (string_of_conjectures conjstr) ^ (string_of_end ())
    1.34      end;
    1.35     
    1.36 -fun clauses2dfg [] probname axioms conjectures funcs preds tfrees = 
    1.37 +fun clauses2dfg [] probname axioms conjectures funcs preds = 
    1.38        let val funcs' = (ResLib.flat_noDup(map funcs_of_cls axioms)) @ funcs
    1.39  	  val preds' = (ResLib.flat_noDup(map preds_of_cls axioms)) @ preds
    1.40        in
    1.41 -	 gen_dfg_file probname axioms conjectures funcs' preds' tfrees 
    1.42 -	 (*(probname, axioms, conjectures, funcs, preds)*)
    1.43 +	 gen_dfg_file probname axioms conjectures funcs' preds' 
    1.44        end
    1.45 - | clauses2dfg (cls::clss) probname axioms conjectures funcs preds tfrees = 
    1.46 + | clauses2dfg (cls::clss) probname axioms conjectures funcs preds = 
    1.47       let val (lits,tfree_lits) = dfg_clause_aux cls
    1.48  	       (*"lits" includes the typing assumptions (TVars)*)
    1.49  	 val cls_id = get_clause_id cls
    1.50 @@ -920,17 +919,10 @@
    1.51  	 val conjectures' = 
    1.52  	     if knd = "conjecture" then (cls::conjectures) else conjectures
    1.53       in
    1.54 -	 clauses2dfg clss probname axioms' conjectures' funcs' preds' tfrees 
    1.55 +	 clauses2dfg clss probname axioms' conjectures' funcs' preds' 
    1.56       end;
    1.57  
    1.58  
    1.59 -fun fileout f str = let val out = TextIO.openOut f
    1.60 -    in
    1.61 -	ResLib.writeln_strs out str; TextIO.closeOut out
    1.62 -    end;
    1.63 -
    1.64 -
    1.65 -
    1.66  fun string_of_arClauseID (ArityClause arcls) =
    1.67      arclause_prefix ^ string_of_int(#clause_id arcls);
    1.68  
    1.69 @@ -997,7 +989,7 @@
    1.70      "input_clause(" ^ string_of_type_clsname (cls_id,ax_name,idx) ^ "," ^ 
    1.71      knd ^ ",[" ^ tfree_lit ^ "]).";
    1.72  
    1.73 -fun tptp_clause_aux (Clause cls) = 
    1.74 +fun tptp_type_lits (Clause cls) = 
    1.75      let val lits = map tptp_literal (#literals cls)
    1.76  	val tvar_lits_strs =
    1.77  	      if !keep_types 
    1.78 @@ -1012,7 +1004,7 @@
    1.79      end; 
    1.80  
    1.81  fun tptp_clause cls =
    1.82 -    let val (lits,tfree_lits) = tptp_clause_aux cls 
    1.83 +    let val (lits,tfree_lits) = tptp_type_lits cls 
    1.84              (*"lits" includes the typing assumptions (TVars)*)
    1.85  	val cls_id = get_clause_id cls
    1.86  	val ax_name = get_axiomName cls
    1.87 @@ -1028,7 +1020,7 @@
    1.88      end;
    1.89  
    1.90  fun clause2tptp cls =
    1.91 -    let val (lits,tfree_lits) = tptp_clause_aux cls 
    1.92 +    let val (lits,tfree_lits) = tptp_type_lits cls 
    1.93              (*"lits" includes the typing assumptions (TVars)*)
    1.94  	val cls_id = get_clause_id cls
    1.95  	val ax_name = get_axiomName cls