src/HOL/Tools/res_clause.ML

 (*FIXME: is this signature necessary? Or maybe define and open a Basic_ResClause?*)
 signature RES_CLAUSE =
   sig
   exception CLAUSE of string * term
   type clause and arityClause and classrelClause
-  type fol_type
-  type typ_var
-  type type_literal
+  datatype fol_type = AtomV of string
+                    | AtomF of string
+                    | Comp of string * fol_type list;
+  datatype fol_term = UVar of string * fol_type
+                    | Fun of string * fol_type list * fol_term list;
+  datatype predicate = Predicate of string * fol_type list * fol_term list;
+  type typ_var and type_literal and literal
+  val literals_of_term: Term.term -> literal list * (typ_var * Term.sort) list
   val add_typs_aux : (typ_var * string list) list -> type_literal list * type_literal list
   val arity_clause_thy: theory -> arityClause list 
   val ascii_of : string -> string
   val bracket_pack : string list -> string
   val classrel_clauses_thy: theory -> classrelClause list 

        ((thm * (string * int)) list * classrelClause list * arityClause list) -> string list
   val fixed_var_prefix : string
   val gen_tptp_cls : int * string * string * string -> string
   val gen_tptp_type_cls : int * string * string * string * int -> string
   val get_axiomName : clause ->  string
+  val get_literals : clause -> literal list
   val init : theory -> unit
   val isMeta : string -> bool
   val isTaut : clause -> bool
   val keep_types : bool ref
   val list_ord : ('a * 'b -> order) -> 'a list * 'b list -> order

 type axiom_name = string;
 type polarity = bool;
 
 (**** Isabelle FOL clauses ****)
 
-type pred_name = string;
-
 datatype typ_var = FOLTVar of indexname | FOLTFree of string;
 
 (*FIXME: give the constructors more sensible names*)
 datatype fol_type = AtomV of string
 		  | AtomF of string

 (*First string is the type class; the second is a TVar or TFfree*)
 datatype type_literal = LTVar of string * string | LTFree of string * string;
 
 datatype fol_term = UVar of string * fol_type
                   | Fun of string * fol_type list * fol_term list;
-datatype predicate = Predicate of pred_name * fol_type list * fol_term list;
+datatype predicate = Predicate of string * fol_type list * fol_term list;
 
 datatype literal = Literal of polarity * predicate;
 
 fun mk_typ_var_sort (TFree(a,s)) = (FOLTFree a,s)
   | mk_typ_var_sort (TVar(v,s)) = (FOLTVar v,s);

 		    kind: kind,
 		    literals: literal list,
 		    types_sorts: (typ_var * sort) list};
 
 fun get_axiomName (Clause cls) = #axiom_name cls;
+
+fun get_literals (Clause cls) = #literals cls;
 
 exception CLAUSE of string * term;
 
 fun isFalse (Literal (pol, Predicate(pname,_,[]))) =
       (pol andalso pname = "c_False") orelse