# HG changeset patch
# User blanchet
# Date 1402940460 -7200
# Node ID 13db1d0787431a47ec9582b9ce17846b70751d51
# Parent  2b6a96cc64c9e67e5a3ab183b346190478df1046
added 'waldmeister_new' as ATP

diff -r 2b6a96cc64c9 -r 13db1d078743 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Jun 16 19:40:59 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Jun 16 19:41:00 2014 +0200
@@ -608,9 +608,8 @@
     SOME s => (SOME Type_Class_Polymorphic, s)
   | NONE =>
     (case try (unprefix "poly_") s of
-      (* It's still unclear whether all TFF1 implementations will support
-         type signatures such as "!>[A : $tType] : $o", with phantom type
-         variables. *)
+      (* It's still unclear whether all TFF1 implementations will support type signatures such as
+         "!>[A : $tType] : $o", with phantom type variables. *)
       SOME s => (SOME (Raw_Polymorphic With_Phantom_Type_Vars), s)
     | NONE =>
       (case try (unprefix "raw_mono_") s of
@@ -651,15 +650,13 @@
              Native (Higher_Order THF_With_Choice, poly, All_Types)
            | _ => raise Same.SAME)
         | ("guards", (SOME poly, _)) =>
-          if (poly = Mangled_Monomorphic andalso
-              level = Undercover_Types) orelse
+          if (poly = Mangled_Monomorphic andalso level = Undercover_Types) orelse
              poly = Type_Class_Polymorphic then
             raise Same.SAME
           else
             Guards (poly, level)
         | ("tags", (SOME poly, _)) =>
-          if (poly = Mangled_Monomorphic andalso
-              level = Undercover_Types) orelse
+          if (poly = Mangled_Monomorphic andalso level = Undercover_Types) orelse
              poly = Type_Class_Polymorphic then
             raise Same.SAME
           else
@@ -668,8 +665,7 @@
           if poly = Type_Class_Polymorphic then raise Same.SAME
           else Guards (poly, Const_Types Without_Ctr_Optim)
         | ("args", (SOME poly, Nonmono_Types (_, Uniform) (* naja *))) =>
-          if poly = Mangled_Monomorphic orelse
-             poly = Type_Class_Polymorphic then
+          if poly = Mangled_Monomorphic orelse poly = Type_Class_Polymorphic then
             raise Same.SAME
           else
             Guards (poly, Const_Types With_Ctr_Optim)
@@ -682,8 +678,7 @@
     Higher_Order THF_Without_Choice
   | adjust_order _ type_enc = type_enc
 
-fun no_type_classes Type_Class_Polymorphic =
-    Raw_Polymorphic With_Phantom_Type_Vars
+fun no_type_classes Type_Class_Polymorphic = Raw_Polymorphic With_Phantom_Type_Vars
   | no_type_classes poly = poly
 
 fun adjust_type_enc (THF (Polymorphic, choice)) (Native (order, poly, level)) =
diff -r 2b6a96cc64c9 -r 13db1d078743 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Jun 16 19:40:59 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Jun 16 19:41:00 2014 +0200
@@ -717,6 +717,15 @@
   (remote_prefix ^ name,
    remotify_config system_name system_versions best_slice o config)
 
+fun gen_remote_waldmeister name =
+  remote_atp name "Waldmeister" ["710"]
+    [("#START OF PROOF", "Proved Goals:")]
+    [(OutOfResources, "Too many function symbols"),
+     (Inappropriate, "****  Unexpected end of file."),
+     (Crashed, "Unrecoverable Segmentation Fault")]
+    Hypothesis
+    (K (((50, ""), CNF_UEQ, "raw_mono_tags??", combsN, false), "") (* FUDGE *))
+
 val explicit_tff0 = TFF Monomorphic
 
 val remote_agsyhol =
@@ -750,14 +759,8 @@
 val remote_e_tofof =
   remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Hypothesis
       (K (((150, ""), explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *))
-val remote_waldmeister =
-  remote_atp waldmeisterN "Waldmeister" ["710"]
-      [("#START OF PROOF", "Proved Goals:")]
-      [(OutOfResources, "Too many function symbols"),
-       (Inappropriate, "****  Unexpected end of file."),
-       (Crashed, "Unrecoverable Segmentation Fault")]
-      Hypothesis
-      (K (((50, ""), CNF_UEQ, "raw_mono_tags??", combsN, false), "") (* FUDGE *))
+val remote_waldmeister = gen_remote_waldmeister waldmeisterN
+val remote_waldmeister_new = gen_remote_waldmeister waldmeister_newN
 
 
 (* Setup *)
@@ -796,7 +799,7 @@
   [agsyhol, alt_ergo, e, e_males, e_par, iprover, iprover_eq, leo2, satallax, spass, vampire,
    z3_tptp, zipperposition, dummy_thf, remote_agsyhol, remote_e, remote_e_sine, remote_e_tofof,
    remote_iprover, remote_iprover_eq, remote_leo2, remote_satallax, remote_vampire, remote_snark,
-   remote_spass_pirate, remote_waldmeister]
+   remote_spass_pirate, remote_waldmeister, remote_waldmeister_new]
 
 val _ = Theory.setup (fold add_atp atps)