Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/res_atp.ML
changeset 18270 27227433cb42
parent 18003 2aecb2d68c00
child 18404 aa27c10a040e 
--- 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 =
isabelle