src/HOL/Tools/res_clause.ML
changeset 19354 aebf9dddccd7
parent 19277 f7602e74d948
child 19443 e32a4703d834
     1.1 --- a/src/HOL/Tools/res_clause.ML	Fri Apr 07 05:12:23 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Fri Apr 07 05:12:51 2006 +0200
     1.3 @@ -55,7 +55,7 @@
     1.4    val tptp_classrelClause : classrelClause -> string
     1.5    val tptp_of_typeLit : type_literal -> string
     1.6    val tptp_tfree_clause : string -> string
     1.7 -  val tptp_write_file: term list -> string -> ((Term.term * (string * int)) list * classrelClause list * arityClause list) -> unit
     1.8 +  val tptp_write_file: term list -> string -> ((thm * (string * int)) list * classrelClause list * arityClause list) -> unit
     1.9    val tvar_prefix : string
    1.10    val types_eq: fol_type list * fol_type list -> (string*string) list * (string*string) list -> bool * ((string*string) list * (string*string) list)
    1.11    val types_ord : fol_type list * fol_type list -> order
    1.12 @@ -620,6 +620,11 @@
    1.13      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.14  						    | NONE => make_axiom_clauses_terms tms;
    1.15      
    1.16 +fun make_axiom_clauses_thms [] = []
    1.17 +  | make_axiom_clauses_thms ((thm,(name,id))::thms) =
    1.18 +    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.19 +						    | NONE => make_axiom_clauses_thms thms;
    1.20 +
    1.21  (**** Isabelle arities ****)
    1.22  
    1.23  exception ARCLAUSE of string;
    1.24 @@ -1030,7 +1035,7 @@
    1.25    let
    1.26      val _ = Output.debug ("Preparing to write the TPTP file " ^ filename)
    1.27      val clss = make_conjecture_clauses terms
    1.28 -    val axclauses' = make_axiom_clauses_terms axclauses
    1.29 +    val axclauses' = make_axiom_clauses_thms axclauses
    1.30      val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp clss)
    1.31      val tfree_clss = map tptp_tfree_clause (foldl (op union_string) [] tfree_litss)
    1.32      val out = TextIO.openOut filename
    1.33 @@ -1043,4 +1048,8 @@
    1.34      TextIO.closeOut out
    1.35    end;
    1.36  
    1.37 +
    1.38 +
    1.39 +
    1.40 +
    1.41  end;