src/HOL/Tools/res_atp.ML
changeset 18270 27227433cb42
parent 18003 2aecb2d68c00
child 18404 aa27c10a040e
equal deleted inserted replaced
18269:3f36e2165e51 18270:27227433cb42
   155       val (clause_arr, axclauses) = ResClasimp.get_clasimp_lemmas ctxt (hd prems) 
   155       val (clause_arr, axclauses) = ResClasimp.get_clasimp_lemmas ctxt (hd prems) 
   156               (*FIXME: hack!! need to consider relevance for all prems*)
   156               (*FIXME: hack!! need to consider relevance for all prems*)
   157       val _ = debug ("claset and simprules total clauses = " ^ 
   157       val _ = debug ("claset and simprules total clauses = " ^ 
   158                      Int.toString (Array.length clause_arr))
   158                      Int.toString (Array.length clause_arr))
   159       val thy = ProofContext.theory_of ctxt
   159       val thy = ProofContext.theory_of ctxt
   160       val classrel_clauses = ResClause.classrel_clauses_thy thy
   160       val classrel_clauses = if !ResClause.keep_types then ResClause.classrel_clauses_thy thy else []
   161       val _ = debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
   161       val _ = debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
   162       val arity_clauses = ResClause.arity_clause_thy thy
   162       val arity_clauses = if !ResClause.keep_types then ResClause.arity_clause_thy thy else []
   163       val _ = debug ("arity clauses = " ^ Int.toString (length arity_clauses))
   163       val _ = debug ("arity clauses = " ^ Int.toString (length arity_clauses))
   164       val write = if !prover = "spass" then dfg_inputs_tfrees else tptp_inputs_tfrees
   164       val write = if !prover = "spass" then dfg_inputs_tfrees else tptp_inputs_tfrees
   165       fun writenext n =
   165       fun writenext n =
   166 	if n=0 then []
   166 	if n=0 then []
   167 	 else
   167 	 else