Deleted unused code
authorpaulson
Thu Jun 14 13:18:24 2007 +0200 (2007-06-14)
changeset 233850ef4f9fc0d09
parent 23384 925b381b4eea
child 23386 9255c1a75ba9
Deleted unused code
src/HOL/Tools/res_clause.ML
     1.1 --- a/src/HOL/Tools/res_clause.ML	Thu Jun 14 13:16:44 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Thu Jun 14 13:18:24 2007 +0200
     1.3 @@ -7,40 +7,28 @@
     1.4  *)
     1.5  
     1.6  (*FIXME: is this signature necessary? Or maybe define and open a Basic_ResClause?*)
     1.7 +(*FIXME: combine with res_hol_clause!*)
     1.8  signature RES_CLAUSE =
     1.9    sig
    1.10    exception CLAUSE of string * term
    1.11 -  type clause and arityClause and classrelClause
    1.12 +  type arityClause and classrelClause
    1.13    datatype fol_type = AtomV of string
    1.14                      | AtomF of string
    1.15                      | Comp of string * fol_type list;
    1.16 -  datatype fol_term = UVar of string
    1.17 -                    | Fun of string * fol_type list * fol_term list;
    1.18 -  datatype predicate = Predicate of string * fol_type list * fol_term list;
    1.19    datatype kind = Axiom | Conjecture;
    1.20    val name_of_kind : kind -> string
    1.21 -  type typ_var and type_literal and literal
    1.22 -  val literals_of_term: Term.term -> literal list * (typ_var * Term.sort) list
    1.23 +  type typ_var and type_literal 
    1.24    val add_typs_aux : (typ_var * string list) list -> type_literal list * type_literal list
    1.25    val ascii_of : string -> string
    1.26    val tptp_pack : string list -> string
    1.27    val make_arity_clauses: theory -> (class list * arityClause list)
    1.28    val make_classrel_clauses: theory -> class list -> class list -> classrelClause list 
    1.29    val clause_prefix : string 
    1.30 -  val clause2tptp : clause -> string * string list
    1.31    val const_prefix : string
    1.32 -  val dfg_write_file:  thm list -> string -> 
    1.33 -       ((thm * (string * int)) list * classrelClause list * arityClause list) -> string list
    1.34    val fixed_var_prefix : string
    1.35    val gen_tptp_cls : int * string * string * string list -> string
    1.36 -  val get_axiomName : clause ->  string
    1.37 -  val get_literals : clause -> literal list
    1.38    val init : theory -> unit
    1.39    val isMeta : string -> bool
    1.40 -  val isTaut : clause -> bool
    1.41 -  val list_ord : ('a * 'b -> order) -> 'a list * 'b list -> order
    1.42 -  val make_axiom_clause : thm -> string * int -> clause option
    1.43 -  val make_conjecture_clauses : thm list -> clause list
    1.44    val make_fixed_const : string -> string		
    1.45    val make_fixed_type_const : string -> string   
    1.46    val make_fixed_type_var : string -> string
    1.47 @@ -59,8 +47,6 @@
    1.48    val tptp_classrelClause : classrelClause -> string
    1.49    val tptp_of_typeLit : type_literal -> string
    1.50    val tptp_tfree_clause : string -> string
    1.51 -  val tptp_write_file: thm list -> string -> 
    1.52 -       ((thm * (string * int)) list * classrelClause list * arityClause list) -> string list
    1.53    val union_all : ''a list list -> ''a list
    1.54    val writeln_strs: TextIO.outstream -> TextIO.vector list -> unit
    1.55    val dfg_sign: bool -> string -> string
    1.56 @@ -209,12 +195,11 @@
    1.57  (***** definitions and functions for FOL clauses, for conversion to TPTP or DFG format. *****)
    1.58  
    1.59  datatype kind = Axiom | Conjecture;
    1.60 +
    1.61  fun name_of_kind Axiom = "axiom"
    1.62    | name_of_kind Conjecture = "negated_conjecture";
    1.63  
    1.64 -type clause_id = int;
    1.65  type axiom_name = string;
    1.66 -type polarity = bool;
    1.67  
    1.68  (**** Isabelle FOL clauses ****)
    1.69  
    1.70 @@ -233,43 +218,12 @@
    1.71  (*First string is the type class; the second is a TVar or TFfree*)
    1.72  datatype type_literal = LTVar of string * string | LTFree of string * string;
    1.73  
    1.74 -datatype fol_term = UVar of string
    1.75 -                  | Fun of string * fol_type list * fol_term list;
    1.76 -datatype predicate = Predicate of string * fol_type list * fol_term list;
    1.77 -
    1.78 -datatype literal = Literal of polarity * predicate;
    1.79 -
    1.80  fun mk_typ_var_sort (TFree(a,s)) = (FOLTFree a,s)
    1.81    | mk_typ_var_sort (TVar(v,s)) = (FOLTVar v,s);
    1.82  
    1.83  
    1.84 -(*A clause has first-order literals and other, type-related literals*)
    1.85 -datatype clause = 
    1.86 -	 Clause of {clause_id: clause_id,
    1.87 -		    axiom_name: axiom_name,
    1.88 -		    th: thm,
    1.89 -		    kind: kind,
    1.90 -		    literals: literal list,
    1.91 -		    types_sorts: (typ_var * sort) list};
    1.92 -
    1.93 -fun get_axiomName (Clause cls) = #axiom_name cls;
    1.94 -
    1.95 -fun get_literals (Clause cls) = #literals cls;
    1.96 -
    1.97  exception CLAUSE of string * term;
    1.98  
    1.99 -fun isFalse (Literal (pol, Predicate(pname,_,[]))) =
   1.100 -      (pol andalso pname = "c_False") orelse
   1.101 -      (not pol andalso pname = "c_True")
   1.102 -  | isFalse _ = false;
   1.103 -
   1.104 -fun isTrue (Literal (pol, Predicate(pname,_,[]))) =
   1.105 -      (pol andalso pname = "c_True") orelse
   1.106 -      (not pol andalso pname = "c_False")
   1.107 -  | isTrue _ = false;
   1.108 -  
   1.109 -fun isTaut (Clause {literals,...}) = exists isTrue literals;  
   1.110 -
   1.111  
   1.112  (*Declarations of the current theory--to allow suppressing types.*)
   1.113  val const_typargs = ref (Library.K [] : (string*typ -> typ list));
   1.114 @@ -300,77 +254,6 @@
   1.115     universal vars, although it is represented as "Free(...)" by Isabelle *)
   1.116  val isMeta = String.isPrefix "METAHYP1_"
   1.117  
   1.118 -fun pred_name_type (Const(c,T)) = (make_fixed_const c, const_types_of (c,T))
   1.119 -  | pred_name_type (Free(x,T))  = 
   1.120 -      if isMeta x then raise CLAUSE("Predicate Not First Order 1", Free(x,T)) 
   1.121 -      else (make_fixed_var x, ([],[]))
   1.122 -  | pred_name_type (v as Var _) = raise CLAUSE("Predicate Not First Order 2", v)
   1.123 -  | pred_name_type t        = raise CLAUSE("Predicate input unexpected", t);
   1.124 -
   1.125 -fun fun_name_type (Const(c,T)) args = (make_fixed_const c, const_types_of (c,T))
   1.126 -  | fun_name_type (Free(x,T)) args  = 
   1.127 -       if isMeta x then raise CLAUSE("Function Not First Order", Free(x,T))
   1.128 -       else (make_fixed_var x, ([],[]))
   1.129 -  | fun_name_type f args = raise CLAUSE("Function Not First Order 1", f);
   1.130 -
   1.131 -(*Convert a term to a fol_term while accumulating sort constraints on the TFrees and
   1.132 -  TVars it contains.*)    
   1.133 -fun term_of (Var(ind_nm,T)) = 
   1.134 -      let val (_,ts) = type_of T
   1.135 -      in (UVar(make_schematic_var ind_nm), ts) end
   1.136 -  | term_of (Free(x,T)) = 
   1.137 -      let val (_,ts) = type_of T
   1.138 -      in
   1.139 -	  if isMeta x then (UVar(make_schematic_var(x,0)), ts)
   1.140 -	  else (Fun(make_fixed_var x, [], []), ts)
   1.141 -      end
   1.142 -  | term_of app = 
   1.143 -      let val (f,args) = strip_comb app
   1.144 -	  val (funName,(contys,ts1)) = fun_name_type f args
   1.145 -	  val (args',ts2) = terms_of args
   1.146 -      in
   1.147 -	  (Fun(funName,contys,args'), union_all (ts1::ts2))
   1.148 -      end
   1.149 -and terms_of ts = ListPair.unzip (map term_of ts)
   1.150 -
   1.151 -(*Create a predicate value, again accumulating sort constraints.*)    
   1.152 -fun pred_of (Const("op =", typ), args) =
   1.153 -      let val (args',ts) = terms_of args
   1.154 -      in
   1.155 -	  (Predicate(make_fixed_const "op =", [], args'),
   1.156 -	   union_all ts)
   1.157 -      end
   1.158 -  | pred_of (pred,args) = 
   1.159 -      let val (pname, (predType,ts1)) = pred_name_type pred
   1.160 -	  val (args',ts2) = terms_of args
   1.161 -      in
   1.162 -	  (Predicate(pname,predType,args'), union_all (ts1::ts2))
   1.163 -      end;
   1.164 -
   1.165 -(*Treatment of literals, possibly negated*)
   1.166 -fun predicate_of ((Const("Not",_) $ P), polarity) = predicate_of (P, not polarity)
   1.167 -  | predicate_of (term,polarity) = (pred_of (strip_comb term), polarity);
   1.168 -
   1.169 -fun literals_of_term1 args (Const("Trueprop",_) $ P) = literals_of_term1 args P
   1.170 -  | literals_of_term1 args (Const("op |",_) $ P $ Q) = 
   1.171 -      literals_of_term1 (literals_of_term1 args P) Q
   1.172 -  | literals_of_term1 (lits, ts) P =
   1.173 -      let val ((pred, ts'), polarity) = predicate_of (P,true)
   1.174 -	  val lits' = Literal(polarity,pred) :: lits
   1.175 -      in
   1.176 -	  (lits', ts union ts')
   1.177 -      end;
   1.178 -
   1.179 -val literals_of_term = literals_of_term1 ([],[]);
   1.180 -
   1.181 -
   1.182 -fun list_ord _ ([],[]) = EQUAL
   1.183 -  | list_ord _ ([],_) = LESS
   1.184 -  | list_ord _ (_,[]) = GREATER
   1.185 -  | list_ord ord (x::xs, y::ys) = 
   1.186 -      (case ord(x,y) of EQUAL => list_ord ord (xs,ys)
   1.187 -	 	      | xy_ord => xy_ord);
   1.188 -		     
   1.189  (*Make literals for sorted type variables*) 
   1.190  fun sorts_on_typs (_, [])   = []
   1.191    | sorts_on_typs (v,  s::ss) = 
   1.192 @@ -391,57 +274,21 @@
   1.193    | add_typs_aux ((FOLTVar indx, s) :: tss) = 
   1.194        let val vs = sorts_on_typs (FOLTVar indx, s)
   1.195  	  val (vss,fss) = add_typs_aux tss
   1.196 -      in
   1.197 -	  (vs union vss, fss)
   1.198 -      end
   1.199 +      in  (vs union vss, fss)  end
   1.200    | add_typs_aux ((FOLTFree x, s) :: tss) =
   1.201        let val fs = sorts_on_typs (FOLTFree x, s)
   1.202  	  val (vss,fss) = add_typs_aux tss
   1.203 -      in
   1.204 -	  (vss, fs union fss)
   1.205 -      end;
   1.206 +      in  (vss, fs union fss)  end;
   1.207  
   1.208  
   1.209  (** make axiom and conjecture clauses. **)
   1.210  
   1.211 -exception MAKE_CLAUSE;
   1.212 -fun make_clause (clause_id, axiom_name, th, kind) =
   1.213 -  let val (lits,types_sorts) = literals_of_term (prop_of th)
   1.214 -  in if forall isFalse lits 
   1.215 -     then error "Problem too trivial for resolution (empty clause)"
   1.216 -     else Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, 
   1.217 -                  kind = kind, literals = lits, types_sorts = types_sorts}
   1.218 -  end;		     
   1.219 -
   1.220  fun get_tvar_strs [] = []
   1.221    | get_tvar_strs ((FOLTVar indx,s)::tss) = 
   1.222        insert (op =) (make_schematic_type_var indx) (get_tvar_strs tss)
   1.223    | get_tvar_strs((FOLTFree x,s)::tss) = get_tvar_strs tss
   1.224  
   1.225 -(* check if a clause is first-order before making a conjecture clause*)
   1.226 -fun make_conjecture_clause n th =
   1.227 -  if Meson.is_fol_term (theory_of_thm th) (prop_of th) 
   1.228 -  then make_clause(n, "conjecture", th, Conjecture)
   1.229 -  else raise CLAUSE("Goal is not FOL", prop_of th);
   1.230 -  
   1.231 -fun make_conjecture_clauses_aux _ [] = []
   1.232 -  | make_conjecture_clauses_aux n (t::ts) =
   1.233 -      make_conjecture_clause n t :: make_conjecture_clauses_aux (n+1) ts
   1.234 -
   1.235 -val make_conjecture_clauses = make_conjecture_clauses_aux 0
   1.236 -
   1.237 -(*before converting an axiom clause to "clause" format, check if it is FOL*)
   1.238 -fun make_axiom_clause th (ax_name,cls_id) =
   1.239 -  if Meson.is_fol_term (theory_of_thm th) (prop_of th) 
   1.240 -  then (SOME (make_clause(cls_id, ax_name, th, Axiom)) handle MAKE_CLAUSE => NONE)
   1.241 -  else (Output.debug (fn () => ("Omitting " ^ ax_name ^ ": Axiom is not FOL")); NONE)
   1.242      
   1.243 -fun make_axiom_clauses [] = []
   1.244 -  | make_axiom_clauses ((th,(name,id))::thms) =
   1.245 -      case make_axiom_clause th (name,id) of 
   1.246 -          SOME cls => if isTaut cls then make_axiom_clauses thms 
   1.247 -                      else (name,cls) :: make_axiom_clauses thms
   1.248 -        | NONE => make_axiom_clauses thms;
   1.249  
   1.250  (**** Isabelle arities ****)
   1.251  
   1.252 @@ -553,21 +400,11 @@
   1.253  
   1.254  fun update_many (tab, keypairs) = foldl (uncurry Symtab.update) tab keypairs;
   1.255  
   1.256 -fun add_predicate_preds (Predicate(pname,tys,tms), preds) = 
   1.257 -  if pname = "equal" then preds (*equality is built-in and requires no declaration*)
   1.258 -  else Symtab.update (pname, length tys + length tms) preds
   1.259 -
   1.260 -fun add_literal_preds (Literal(_,pred), preds) = add_predicate_preds (pred,preds)
   1.261 -
   1.262  fun add_type_sort_preds ((FOLTVar indx,s), preds) = 
   1.263        update_many (preds, map pred_of_sort (sorts_on_typs (FOLTVar indx, s)))
   1.264    | add_type_sort_preds ((FOLTFree x,s), preds) =
   1.265        update_many (preds, map pred_of_sort (sorts_on_typs (FOLTFree x, s)));
   1.266  
   1.267 -fun add_clause_preds (Clause {literals, types_sorts, ...}, preds) =
   1.268 -  foldl add_literal_preds (foldl add_type_sort_preds preds types_sorts) literals
   1.269 -  handle Symtab.DUP a => raise ERROR ("predicate " ^ a ^ " has multiple arities")
   1.270 -
   1.271  fun add_classrelClause_preds (ClassrelClause {subclass,superclass,...}, preds) =
   1.272    Symtab.update (subclass,1) (Symtab.update (superclass,1) preds);
   1.273  
   1.274 @@ -579,14 +416,6 @@
   1.275        fun upd (class,preds) = Symtab.update (class,1) preds
   1.276    in  foldl upd preds classes  end;
   1.277  
   1.278 -fun preds_of_clauses clauses clsrel_clauses arity_clauses = 
   1.279 -  Symtab.dest
   1.280 -    (foldl add_classrelClause_preds 
   1.281 -      (foldl add_arityClause_preds
   1.282 -        (foldl add_clause_preds Symtab.empty clauses)
   1.283 -        arity_clauses)
   1.284 -      clsrel_clauses)
   1.285 -
   1.286  (*** Find occurrences of functions in clauses ***)
   1.287  
   1.288  fun add_foltype_funcs (AtomV _, funcs) = funcs
   1.289 @@ -594,18 +423,6 @@
   1.290    | add_foltype_funcs (Comp(a,tys), funcs) = 
   1.291        foldl add_foltype_funcs (Symtab.update (a, length tys) funcs) tys;
   1.292  
   1.293 -fun add_folterm_funcs (UVar _, funcs) = funcs
   1.294 -  | add_folterm_funcs (Fun(a,tys,tms), funcs) = 
   1.295 -      foldl add_foltype_funcs 
   1.296 -	    (foldl add_folterm_funcs (Symtab.update (a, length tys + length tms) funcs) 
   1.297 -	           tms) 
   1.298 -	    tys
   1.299 -
   1.300 -fun add_predicate_funcs (Predicate(_,tys,tms), funcs) = 
   1.301 -    foldl add_foltype_funcs (foldl add_folterm_funcs funcs tms) tys;
   1.302 -
   1.303 -fun add_literal_funcs (Literal(_,pred), funcs) = add_predicate_funcs (pred,funcs)
   1.304 -
   1.305  (*TFrees are recorded as constants*)
   1.306  fun add_type_sort_funcs ((FOLTVar _, _), funcs) = funcs
   1.307    | add_type_sort_funcs ((FOLTFree a, _), funcs) = 
   1.308 @@ -615,44 +432,15 @@
   1.309    let val TConsLit (_, tcons, tvars) = conclLit
   1.310    in  Symtab.update (tcons, length tvars) funcs  end;
   1.311  
   1.312 -fun add_clause_funcs (Clause {literals, types_sorts, ...}, funcs) =
   1.313 -  foldl add_literal_funcs (foldl add_type_sort_funcs funcs types_sorts)
   1.314 -       literals
   1.315 -  handle Symtab.DUP a => raise ERROR ("function " ^ a ^ " has multiple arities")
   1.316 -
   1.317  (*This type can be overlooked because it is built-in...*)
   1.318  val init_functab = Symtab.update ("tc_itself", 1) Symtab.empty;
   1.319  
   1.320 -fun funcs_of_clauses clauses arity_clauses = 
   1.321 -  Symtab.dest (foldl add_arityClause_funcs 
   1.322 -                     (foldl add_clause_funcs init_functab clauses)
   1.323 -                     arity_clauses)
   1.324 -
   1.325  
   1.326  (**** String-oriented operations ****)
   1.327  
   1.328 -fun string_of_term (UVar x) = x
   1.329 -  | string_of_term (Fun (name,typs,terms)) = 
   1.330 -      name ^ (paren_pack (map string_of_term terms @ map string_of_fol_type typs));
   1.331 -
   1.332 -fun string_of_pair [t1,t2] = (string_of_term t1, string_of_term t2)
   1.333 -  | string_of_pair _ = raise ERROR ("equality predicate requires two arguments");
   1.334 -
   1.335 -fun string_of_equality ts =
   1.336 -  let val (s1,s2) = string_of_pair ts
   1.337 -  in "equal(" ^ s1 ^ "," ^ s2 ^ ")" end;
   1.338 -
   1.339 -(* before output the string of the predicate, check if the predicate corresponds to an equality or not. *)
   1.340 -fun string_of_predicate (Predicate("equal",_,ts)) = string_of_equality ts
   1.341 -  | string_of_predicate (Predicate(name,typs,ts)) = 
   1.342 -      name ^ (paren_pack (map string_of_term ts @ map string_of_fol_type typs));
   1.343 -
   1.344  fun string_of_clausename (cls_id,ax_name) = 
   1.345      clause_prefix ^ ascii_of ax_name ^ "_" ^ Int.toString cls_id;
   1.346  
   1.347 -fun clause_name_of (cls_id,ax_name) = 
   1.348 -    ascii_of ax_name ^ "_" ^ Int.toString cls_id;
   1.349 -
   1.350  fun string_of_type_clsname (cls_id,ax_name,idx) = 
   1.351      string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx);
   1.352  
   1.353 @@ -666,8 +454,6 @@
   1.354  fun dfg_sign true s = s
   1.355    | dfg_sign false s = "not(" ^ s ^ ")"  
   1.356  
   1.357 -fun dfg_literal (Literal(pol,pred)) = dfg_sign pol (string_of_predicate pred)
   1.358 -
   1.359  fun dfg_of_typeLit (LTVar (s,ty)) = "not(" ^ s ^ "(" ^ ty ^ "))"
   1.360    | dfg_of_typeLit (LTFree (s,ty)) = s ^ "(" ^ ty ^ ")";
   1.361   
   1.362 @@ -680,31 +466,6 @@
   1.363      dfg_forall vars ("or(" ^ lits ^ ")") ^ ",\n" ^ 
   1.364      string_of_clausename (cls_id,ax_name) ^  ").\n\n";
   1.365  
   1.366 -fun dfg_clause_aux (Clause{literals, types_sorts, ...}) = 
   1.367 -  let val (tvar_lits,tfree_lits) = add_typs_aux types_sorts
   1.368 -  in  (map dfg_of_typeLit tvar_lits @ map dfg_literal literals, 
   1.369 -       map dfg_of_typeLit tfree_lits)
   1.370 -  end; 
   1.371 -
   1.372 -fun dfg_folterms (Literal(pol,pred)) = 
   1.373 -  let val Predicate (_, _, folterms) = pred
   1.374 -  in  folterms  end
   1.375 -
   1.376 -fun get_uvars (UVar a) = [a] 
   1.377 -  | get_uvars (Fun (_,typ,tlist)) = union_all(map get_uvars tlist)
   1.378 -
   1.379 -fun dfg_vars (Clause {literals,...}) =
   1.380 -  union_all (map get_uvars (List.concat (map dfg_folterms literals)))
   1.381 -
   1.382 -fun clause2dfg (cls as Clause{axiom_name,clause_id,kind,types_sorts,...}) =
   1.383 -    let val (lits,tfree_lits) = dfg_clause_aux cls 
   1.384 -            (*"lits" includes the typing assumptions (TVars)*)
   1.385 -        val vars = dfg_vars cls
   1.386 -        val tvars = get_tvar_strs types_sorts
   1.387 -	val cls_str = gen_dfg_cls(clause_id, axiom_name, name_of_kind kind, 
   1.388 -	                           commas lits, tvars@vars) 
   1.389 -    in (cls_str, tfree_lits) end;
   1.390 -
   1.391  fun string_of_arity (name, num) =  "(" ^ name ^ "," ^ Int.toString num ^ ")"
   1.392  
   1.393  fun string_of_preds [] = ""
   1.394 @@ -747,37 +508,6 @@
   1.395        string_of_ar axiom_name ^ ").\n\n"
   1.396    end;
   1.397  
   1.398 -(* write out a subgoal in DFG format to the file "xxxx_N"*)
   1.399 -fun dfg_write_file thms filename (ax_tuples,classrel_clauses,arity_clauses) = 
   1.400 -  let 
   1.401 -    val _ = Output.debug (fn () => ("Preparing to write the DFG file " ^ filename))
   1.402 -    val _ = dfg_format := true
   1.403 -    val conjectures = make_conjecture_clauses thms
   1.404 -    val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses ax_tuples)
   1.405 -    val (dfg_clss, tfree_litss) = ListPair.unzip (map clause2dfg conjectures)
   1.406 -    val clss = conjectures @ axclauses
   1.407 -    val funcs = funcs_of_clauses clss arity_clauses
   1.408 -    and preds = preds_of_clauses clss classrel_clauses arity_clauses
   1.409 -    and probname = Path.implode (Path.base (Path.explode filename))
   1.410 -    val (axstrs, _) = ListPair.unzip (map clause2dfg axclauses)
   1.411 -    val tfree_clss = map dfg_tfree_clause (union_all tfree_litss) 
   1.412 -    val out = TextIO.openOut filename
   1.413 -  in
   1.414 -    TextIO.output (out, string_of_start probname); 
   1.415 -    TextIO.output (out, string_of_descrip probname); 
   1.416 -    TextIO.output (out, string_of_symbols (string_of_funcs funcs) (string_of_preds preds)); 
   1.417 -    TextIO.output (out, "list_of_clauses(axioms,cnf).\n");
   1.418 -    writeln_strs out axstrs;
   1.419 -    List.app (curry TextIO.output out o dfg_classrelClause) classrel_clauses;
   1.420 -    List.app (curry TextIO.output out o dfg_arity_clause) arity_clauses;
   1.421 -    TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n");
   1.422 -    writeln_strs out tfree_clss;
   1.423 -    writeln_strs out dfg_clss;
   1.424 -    TextIO.output (out, "end_of_list.\n\nend_problem.\n");
   1.425 -    TextIO.closeOut out;
   1.426 -    clnames
   1.427 -  end;
   1.428 -
   1.429  
   1.430  (**** Produce TPTP files ****)
   1.431  
   1.432 @@ -785,14 +515,6 @@
   1.433  fun tptp_sign true s = s
   1.434    | tptp_sign false s = "~ " ^ s
   1.435  
   1.436 -fun tptp_of_equality pol ts =
   1.437 -  let val (s1,s2) = string_of_pair ts
   1.438 -      val eqop = if pol then " = " else " != "
   1.439 -  in  s1 ^ eqop ^ s2  end;
   1.440 -
   1.441 -fun tptp_literal (Literal(pol,Predicate("equal",_,ts))) = tptp_of_equality pol ts
   1.442 -  | tptp_literal (Literal(pol,pred)) = tptp_sign pol (string_of_predicate pred);
   1.443 -
   1.444  fun tptp_of_typeLit (LTVar (s,ty))  = tptp_sign false (s ^ "(" ^ ty ^ ")")
   1.445    | tptp_of_typeLit (LTFree (s,ty)) = tptp_sign true  (s ^ "(" ^ ty ^ ")");
   1.446   
   1.447 @@ -800,21 +522,6 @@
   1.448      "cnf(" ^ string_of_clausename (cls_id,ax_name) ^ "," ^ 
   1.449      name_of_kind knd ^ "," ^ tptp_pack lits ^ ").\n";
   1.450  
   1.451 -fun tptp_type_lits (Clause {literals, types_sorts, ...}) = 
   1.452 -  let val (tvar_lits,tfree_lits) = add_typs_aux types_sorts
   1.453 -  in
   1.454 -      (map tptp_of_typeLit tvar_lits @ map tptp_literal literals,
   1.455 -       map tptp_of_typeLit tfree_lits)
   1.456 -  end; 
   1.457 -
   1.458 -fun clause2tptp (cls as Clause {clause_id, axiom_name, kind, ...}) =
   1.459 -    let val (lits,tfree_lits) = tptp_type_lits cls 
   1.460 -            (*"lits" includes the typing assumptions (TVars)*)
   1.461 -	val cls_str = gen_tptp_cls(clause_id, axiom_name, kind, lits) 
   1.462 -    in
   1.463 -	(cls_str,tfree_lits) 
   1.464 -    end;
   1.465 -
   1.466  fun tptp_tfree_clause tfree_lit =
   1.467      "cnf(" ^ "tfree_tcs," ^ "negated_conjecture" ^ "," ^ tptp_pack[tfree_lit] ^ ").\n";
   1.468      
   1.469 @@ -834,24 +541,4 @@
   1.470  fun tptp_classrelClause (ClassrelClause {axiom_name,subclass,superclass,...}) =
   1.471    "cnf(" ^ axiom_name ^ ",axiom," ^ tptp_classrelLits subclass superclass ^ ").\n" 
   1.472  
   1.473 -(* write out a subgoal as tptp clauses to the file "xxxx_N"*)
   1.474 -fun tptp_write_file thms filename (ax_tuples,classrel_clauses,arity_clauses) =
   1.475 -  let
   1.476 -    val _ = Output.debug (fn () => ("Preparing to write the TPTP file " ^ filename))
   1.477 -    val _ = dfg_format := false
   1.478 -    val clss = make_conjecture_clauses thms
   1.479 -    val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses ax_tuples)
   1.480 -    val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp clss)
   1.481 -    val tfree_clss = map tptp_tfree_clause (foldl (op union_string) [] tfree_litss)
   1.482 -    val out = TextIO.openOut filename
   1.483 -  in
   1.484 -    List.app (curry TextIO.output out o #1 o clause2tptp) axclauses;
   1.485 -    writeln_strs out tfree_clss;
   1.486 -    writeln_strs out tptp_clss;
   1.487 -    List.app (curry TextIO.output out o tptp_classrelClause) classrel_clauses;
   1.488 -    List.app (curry TextIO.output out o tptp_arity_clause) arity_clauses;
   1.489 -    TextIO.closeOut out;
   1.490 -    clnames
   1.491 -  end;
   1.492 -
   1.493  end;