1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Tue Apr 18 05:37:43 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Tue Apr 18 05:38:18 2006 +0200
     1.3 @@ -478,8 +478,9 @@
     1.4  
     1.5  
     1.6  (* making axiom and conjecture clauses *)
     1.7 -fun make_axiom_clause term (ax_name,cls_id) =
     1.8 -    let val term' = comb_of term
     1.9 +fun make_axiom_clause thm (ax_name,cls_id) =
    1.10 +    let val term = prop_of thm
    1.11 +	val term' = comb_of term
    1.12  	val (lits,ctypes_sorts) = literals_of_term term'
    1.13  	val lits' = sort_lits lits
    1.14  	val (ctvar_lits,ctfree_lits) = ResClause.add_typs_aux ctypes_sorts
    1.15 @@ -488,25 +489,18 @@
    1.16  		    lits',ctypes_sorts,ctvar_lits,ctfree_lits)
    1.17      end;
    1.18  
    1.19 -fun make_axiom_clauses_terms [] = []
    1.20 -  | make_axiom_clauses_terms ((tm,(name,id))::tms) =
    1.21 -    let val cls = make_axiom_clause tm (name,id)
    1.22 -	val clss = make_axiom_clauses_terms tms
    1.23 +fun make_axiom_clauses [] = []
    1.24 +  | make_axiom_clauses ((thm,(name,id))::thms) =
    1.25 +    let val cls = make_axiom_clause thm (name,id)
    1.26 +	val clss = make_axiom_clauses thms
    1.27      in
    1.28  	if isTaut cls then clss else (cls::clss)
    1.29      end;
    1.30  
    1.31 -fun make_axiom_clauses_thms [] = []
    1.32 -  | make_axiom_clauses_thms ((thm,(name,id))::thms) =
    1.33 -    let val cls = make_axiom_clause (prop_of thm) (name,id)
    1.34 -	val clss = make_axiom_clauses_thms thms
    1.35 -    in
    1.36 -	if isTaut cls then clss else (cls::clss)
    1.37 -    end;
    1.38  
    1.39 -
    1.40 -fun make_conjecture_clause n t =
    1.41 -    let val t' = comb_of t
    1.42 +fun make_conjecture_clause n thm =
    1.43 +    let val t = prop_of thm
    1.44 +	val t' = comb_of t
    1.45  	val (lits,ctypes_sorts) = literals_of_term t'
    1.46  	val (ctvar_lits,ctfree_lits) = ResClause.add_typs_aux ctypes_sorts
    1.47      in
    1.48 @@ -779,9 +773,9 @@
    1.49  
    1.50  (* write TPTP format to a single file *)
    1.51  (* when "get_helper_clauses" is called, "include_combS" and "include_min_comb" should have correct values already *)
    1.52 -fun tptp_write_file terms filename (axclauses,classrel_clauses,arity_clauses) helpers =
    1.53 -    let val clss = make_conjecture_clauses terms
    1.54 -	val axclauses' = make_axiom_clauses_thms axclauses
    1.55 +fun tptp_write_file thms filename (axclauses,classrel_clauses,arity_clauses) helpers =
    1.56 +    let val clss = make_conjecture_clauses thms
    1.57 +	val axclauses' = make_axiom_clauses axclauses
    1.58  	val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp clss)
    1.59  	val tfree_clss = map ResClause.tptp_tfree_clause (foldl (op union_string) [] tfree_litss)
    1.60  	val out = TextIO.openOut filename