1.1 --- a/src/HOL/Tools/res_clause.ML	Tue Apr 18 05:36:38 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Tue Apr 18 05:37:43 2006 +0200
     1.3 @@ -34,8 +34,8 @@
     1.4    val isTaut : clause -> bool
     1.5    val keep_types : bool ref
     1.6    val list_ord : ('a * 'b -> order) -> 'a list * 'b list -> order
     1.7 -  val make_axiom_clause : Term.term -> string * int -> clause option
     1.8 -  val make_conjecture_clauses : term list -> clause list
     1.9 +  val make_axiom_clause : thm -> string * int -> clause option
    1.10 +  val make_conjecture_clauses : thm list -> clause list
    1.11    val make_fixed_const : string -> string		
    1.12    val make_fixed_type_const : string -> string   
    1.13    val make_fixed_type_var : string -> string
    1.14 @@ -55,7 +55,7 @@
    1.15    val tptp_classrelClause : classrelClause -> string
    1.16    val tptp_of_typeLit : type_literal -> string
    1.17    val tptp_tfree_clause : string -> string
    1.18 -  val tptp_write_file: term list -> string -> ((thm * (string * int)) list * classrelClause list * arityClause list) -> unit
    1.19 +  val tptp_write_file: thm list -> string -> ((thm * (string * int)) list * classrelClause list * arityClause list) -> unit
    1.20    val tvar_prefix : string
    1.21    val types_eq: fol_type list * fol_type list -> (string*string) list * (string*string) list -> bool * ((string*string) list * (string*string) list)
    1.22    val types_ord : fol_type list * fol_type list -> order
    1.23 @@ -570,8 +570,9 @@
    1.24    | get_tvar_strs((FOLTFree x,s)::tss) = get_tvar_strs tss
    1.25  
    1.26  (* check if a clause is first-order before making a conjecture clause*)
    1.27 -fun make_conjecture_clause n t =
    1.28 -    let val _ = check_is_fol_term t
    1.29 +fun make_conjecture_clause n thm =
    1.30 +    let val t = prop_of thm
    1.31 +	val _ = check_is_fol_term t
    1.32  	    handle TERM("check_is_fol_term",_) => raise CLAUSE("Goal is not FOL",t)
    1.33  	val (lits,types_sorts) = literals_of_term t
    1.34      in
    1.35 @@ -601,8 +602,9 @@
    1.36    | too_general_lit _ = false;
    1.37  
    1.38  (*before converting an axiom clause to "clause" format, check if it is FOL*)
    1.39 -fun make_axiom_clause term (ax_name,cls_id) =
    1.40 -    let val (lits,types_sorts) = literals_of_term term
    1.41 +fun make_axiom_clause thm (ax_name,cls_id) =
    1.42 +    let val term = prop_of thm
    1.43 +	val (lits,types_sorts) = literals_of_term term
    1.44      in 
    1.45  	if not (Meson.is_fol_term term) then
    1.46  	   (Output.debug ("Omitting " ^ ax_name ^ ": Axiom is not FOL"); 
    1.47 @@ -615,15 +617,10 @@
    1.48      handle CLAUSE _ => NONE;
    1.49  
    1.50  
    1.51 -fun make_axiom_clauses_terms [] = []
    1.52 -  | make_axiom_clauses_terms ((tm,(name,id))::tms) =
    1.53 -    case make_axiom_clause tm (name,id) of SOME cls => if isTaut cls then make_axiom_clauses_terms tms else cls :: make_axiom_clauses_terms tms
    1.54 -						    | NONE => make_axiom_clauses_terms tms;
    1.55 -    
    1.56 -fun make_axiom_clauses_thms [] = []
    1.57 -  | make_axiom_clauses_thms ((thm,(name,id))::thms) =
    1.58 -    case make_axiom_clause (prop_of thm) (name,id) of SOME cls => if isTaut cls then make_axiom_clauses_thms thms else cls :: make_axiom_clauses_thms thms
    1.59 -						    | NONE => make_axiom_clauses_thms thms;
    1.60 +fun make_axiom_clauses [] = []
    1.61 +  | make_axiom_clauses ((thm,(name,id))::thms) =
    1.62 +    case make_axiom_clause thm (name,id) of SOME cls => if isTaut cls then make_axiom_clauses thms else cls :: make_axiom_clauses thms
    1.63 +						    | NONE => make_axiom_clauses thms;
    1.64  
    1.65  (**** Isabelle arities ****)
    1.66  
    1.67 @@ -934,7 +931,7 @@
    1.68  fun dfg_write_file ths filename (axclauses,classrel_clauses,arity_clauses) = 
    1.69    let 
    1.70      val _ = Output.debug ("Preparing to write the DFG file " ^ filename)
    1.71 -    val conjectures = make_conjecture_clauses (map prop_of ths)
    1.72 +    val conjectures = make_conjecture_clauses ths
    1.73      val (dfg_clss, tfree_litss) = ListPair.unzip (map clause2dfg conjectures)
    1.74      val clss = conjectures @ axclauses
    1.75      val funcs = funcs_of_clauses clss arity_clauses
    1.76 @@ -1031,11 +1028,11 @@
    1.77    "input_clause(" ^ axiom_name ^ ",axiom," ^ tptp_classrelLits subclass superclass ^ ").\n" 
    1.78  
    1.79  (* write out a subgoal as tptp clauses to the file "xxxx_N"*)
    1.80 -fun tptp_write_file terms filename (axclauses,classrel_clauses,arity_clauses) =
    1.81 +fun tptp_write_file thms filename (axclauses,classrel_clauses,arity_clauses) =
    1.82    let
    1.83      val _ = Output.debug ("Preparing to write the TPTP file " ^ filename)
    1.84 -    val clss = make_conjecture_clauses terms
    1.85 -    val axclauses' = make_axiom_clauses_thms axclauses
    1.86 +    val clss = make_conjecture_clauses thms
    1.87 +    val axclauses' = make_axiom_clauses axclauses
    1.88      val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp clss)
    1.89      val tfree_clss = map tptp_tfree_clause (foldl (op union_string) [] tfree_litss)
    1.90      val out = TextIO.openOut filename