src/HOL/Tools/ATP/atp_systems.ML

--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Sep 06 22:41:35 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Sep 07 09:10:41 2011 +0200
@@ -222,11 +222,11 @@
      let val method = effective_e_weight_method ctxt in
        (* FUDGE *)
        if method = e_smartN then
-         [(0.333, (true, (500, FOF, "mono_tags?", e_fun_weightN))),
-          (0.334, (true, (50, FOF, "mono_guards?", e_fun_weightN))),
-          (0.333, (true, (1000, FOF, "mono_tags?", e_sym_offset_weightN)))]
+         [(0.333, (true, (500, FOF, "mono_tags??", e_fun_weightN))),
+          (0.334, (true, (50, FOF, "mono_guards??", e_fun_weightN))),
+          (0.333, (true, (1000, FOF, "mono_tags??", e_sym_offset_weightN)))]
        else
-         [(1.0, (true, (500, FOF, "mono_tags?", method)))]
+         [(1.0, (true, (500, FOF, "mono_tags??", method)))]
      end}
 
 val e = (eN, e_config)
@@ -304,9 +304,9 @@
    prem_kind = Conjecture,
    best_slices = fn ctxt =>
      (* FUDGE *)
-     [(0.333, (false, (150, FOF, "mono_tags", sosN))),
-      (0.333, (false, (300, FOF, "poly_tags?", sosN))),
-      (0.334, (true, (50, FOF, "mono_tags?", no_sosN)))]
+     [(0.333, (false, (150, FOF, "mono_tags??", sosN))),
+      (0.333, (false, (300, FOF, "poly_tags??", sosN))),
+      (0.334, (true, (50, FOF, "mono_tags??", no_sosN)))]
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I)}
 
@@ -349,11 +349,11 @@
    best_slices = fn ctxt =>
      (* FUDGE *)
      (if is_old_vampire_version () then
-        [(0.333, (false, (150, FOF, "poly_guards", sosN))),
-         (0.333, (false, (500, FOF, "mono_tags?", sosN))),
-         (0.334, (true, (50, FOF, "mono_guards?", no_sosN)))]
+        [(0.333, (false, (150, FOF, "poly_guards??", sosN))),
+         (0.333, (false, (500, FOF, "mono_tags??", sosN))),
+         (0.334, (true, (50, FOF, "mono_guards??", no_sosN)))]
       else
-        [(0.333, (false, (150, vampire_tff0, "poly_guards", sosN))),
+        [(0.333, (false, (150, vampire_tff0, "poly_guards??", sosN))),
          (0.333, (false, (500, vampire_tff0, "mono_simple", sosN))),
          (0.334, (true, (50, vampire_tff0, "mono_simple", no_sosN)))])
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
@@ -490,7 +490,7 @@
 
 val remote_e =
   remotify_atp e "EP" ["1.0", "1.1", "1.2"]
-               (K (750, FOF, "mono_tags?") (* FUDGE *))
+               (K (750, FOF, "mono_tags??") (* FUDGE *))
 val remote_leo2 =
   remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
                (K (100, leo2_thf0, "mono_simple_higher") (* FUDGE *))
@@ -499,13 +499,13 @@
                (K (100, satallax_thf0, "mono_simple_higher") (* FUDGE *))
 val remote_vampire =
   remotify_atp vampire "Vampire" ["1.8"]
-               (K (250, FOF, "mono_guards?") (* FUDGE *))
+               (K (250, FOF, "mono_guards??") (* FUDGE *))
 val remote_z3_tptp =
   remotify_atp z3_tptp "Z3" ["3.0"]
                (K (250, z3_tff0, "mono_simple") (* FUDGE *))
 val remote_e_sine =
   remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
-             Conjecture (K (500, FOF, "mono_guards?") (* FUDGE *))
+             Conjecture (K (500, FOF, "mono_guards??") (* FUDGE *))
 val remote_snark =
   remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
              [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
@@ -519,7 +519,7 @@
              [(OutOfResources, "Too many function symbols"),
               (Crashed, "Unrecoverable Segmentation Fault")]
              Hypothesis Hypothesis
-             (K (50, CNF_UEQ, "mono_tags?") (* FUDGE *))
+             (K (50, CNF_UEQ, "mono_tags??") (* FUDGE *))
 
 (* Setup *)