Only output arities and class relations if !ResClause.keep_types is true.
authormengj
Mon Nov 28 07:12:01 2005 +0100 (2005-11-28)
changeset 1827027227433cb42
parent 18269 3f36e2165e51
child 18271 0e9a851db989
Only output arities and class relations if !ResClause.keep_types is true.
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Mon Nov 28 05:03:00 2005 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Mon Nov 28 07:12:01 2005 +0100
     1.3 @@ -157,9 +157,9 @@
     1.4        val _ = debug ("claset and simprules total clauses = " ^ 
     1.5                       Int.toString (Array.length clause_arr))
     1.6        val thy = ProofContext.theory_of ctxt
     1.7 -      val classrel_clauses = ResClause.classrel_clauses_thy thy
     1.8 +      val classrel_clauses = if !ResClause.keep_types then ResClause.classrel_clauses_thy thy else []
     1.9        val _ = debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
    1.10 -      val arity_clauses = ResClause.arity_clause_thy thy
    1.11 +      val arity_clauses = if !ResClause.keep_types then ResClause.arity_clause_thy thy else []
    1.12        val _ = debug ("arity clauses = " ^ Int.toString (length arity_clauses))
    1.13        val write = if !prover = "spass" then dfg_inputs_tfrees else tptp_inputs_tfrees
    1.14        fun writenext n =