1.1 --- a/src/HOL/Tools/res_atp.ML	Thu Oct 13 11:58:22 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Oct 14 10:19:50 2005 +0200
     1.3 @@ -67,7 +67,7 @@
     1.4  (* write out a subgoal as tptp clauses to the file "xxxx_N"*)
     1.5  fun tptp_inputs_tfrees thms pf n (axclauses,classrel_clauses,arity_clauses) =
     1.6    let
     1.7 -    val clss = map (ResClause.make_conjecture_clause_thm) thms
     1.8 +    val clss = ResClause.make_conjecture_clauses thms
     1.9      val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
    1.10      val tfree_clss = map ResClause.tfree_clause (foldl (op union_string) [] tfree_litss)
    1.11      val classrel_cls = map ResClause.tptp_classrelClause classrel_clauses
    1.12 @@ -81,7 +81,7 @@
    1.13  
    1.14  (* write out a subgoal in DFG format to the file "xxxx_N"*)
    1.15  fun dfg_inputs_tfrees thms pf n (axclauses,classrel_clauses,arity_clauses) = 
    1.16 -    let val clss = map (ResClause.make_conjecture_clause_thm) thms
    1.17 +    let val clss = ResClause.make_conjecture_clauses thms
    1.18          (*FIXME: classrel_clauses and arity_clauses*)
    1.19          val probN = ResClause.clauses2dfg clss (!problem_name ^ "_" ^ Int.toString n)
    1.20                          axclauses [] [] []    
    1.21 @@ -159,9 +159,9 @@
    1.22        val _ = debug ("claset and simprules total clauses = " ^ 
    1.23                       Int.toString (Array.length clause_arr))
    1.24        val thy = ProofContext.theory_of ctxt
    1.25 -      val classrel_clauses = ResTypesSorts.classrel_clauses_thy thy
    1.26 +      val classrel_clauses = ResClause.classrel_clauses_thy thy
    1.27        val _ = debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
    1.28 -      val arity_clauses = ResTypesSorts.arity_clause_thy thy
    1.29 +      val arity_clauses = ResClause.arity_clause_thy thy
    1.30        val _ = debug ("arity clauses = " ^ Int.toString (length arity_clauses))
    1.31        val write = if !prover = "spass" then dfg_inputs_tfrees else tptp_inputs_tfrees
    1.32        fun writenext n =