# HG changeset patch
# User mengj
# Date 1133158321 -3600
# Node ID 27227433cb42ca2dc1ee708fff0c6e74488dbd16
# Parent  3f36e2165e51eb7df5aba98fdb49e0a3f5dab127
Only output arities and class relations if !ResClause.keep_types is true.

diff -r 3f36e2165e51 -r 27227433cb42 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Mon Nov 28 05:03:00 2005 +0100
+++ b/src/HOL/Tools/res_atp.ML	Mon Nov 28 07:12:01 2005 +0100
@@ -157,9 +157,9 @@
       val _ = debug ("claset and simprules total clauses = " ^ 
                      Int.toString (Array.length clause_arr))
       val thy = ProofContext.theory_of ctxt
-      val classrel_clauses = ResClause.classrel_clauses_thy thy
+      val classrel_clauses = if !ResClause.keep_types then ResClause.classrel_clauses_thy thy else []
       val _ = debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
-      val arity_clauses = ResClause.arity_clause_thy thy
+      val arity_clauses = if !ResClause.keep_types then ResClause.arity_clause_thy thy else []
       val _ = debug ("arity clauses = " ^ Int.toString (length arity_clauses))
       val write = if !prover = "spass" then dfg_inputs_tfrees else tptp_inputs_tfrees
       fun writenext n =