better default type system for Waldmeister, with fewer predicates (for types or type classes)
authorblanchet
Wed, 08 Jun 2011 16:20:18 +0200
changeset 43288 7a4eebdebb23
parent 43274 ad4611809a29
child 43289 0f2bbcfaf208
better default type system for Waldmeister, with fewer predicates (for types or type classes)
src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Jun 08 13:45:01 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Jun 08 16:20:18 2011 +0200
@@ -432,7 +432,7 @@
              [(OutOfResources, "Too many function symbols"),
               (Crashed, "Unrecoverable Segmentation Fault")]
              Hypothesis Hypothesis [CNF_UEQ]
-             (K (50, ["poly_args"]) (* FUDGE *))
+             (K (50, ["mangled_args", "mangled_tags?"]) (* FUDGE *))
 
 (* Setup *)