# HG changeset patch
# User blanchet
# Date 1305793453 -7200
# Node ID b48529f4188812cc98faf50359a8102acfc24749
# Parent  d99167ac4f8af07afde93689bc80188fa3c840fe
renamed "simple_types" to "simple"

diff -r d99167ac4f8a -r b48529f41888 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu May 19 10:24:13 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu May 19 10:24:13 2011 +0200
@@ -406,14 +406,14 @@
 val remote_z3_atp = remotify_atp z3_atp "Z3" ["2.18"]
 val remote_tofof_e =
   remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config)
-             Axiom Conjecture [Tff] (K (200, ["simple_types"]) (* FUDGE *))
+             Axiom Conjecture [Tff] (K (200, ["simple"]) (* FUDGE *))
 val remote_sine_e =
   remote_atp sine_eN "SInE" ["0.4"] [] [] Axiom Conjecture [Fof]
              (K (500, ["poly_tags_heavy!", "poly_tags_heavy"]) (* FUDGE *))
 val remote_snark =
   remote_atp snarkN "SNARK" ["20080805r024"]
              [("refutation.", "end_refutation.")] [] Hypothesis Conjecture
-             [Tff, Fof] (K (250, ["simple_types"]) (* FUDGE *))
+             [Tff, Fof] (K (250, ["simple"]) (* FUDGE *))
 
 (* Setup *)
 
diff -r d99167ac4f8a -r b48529f41888 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 19 10:24:13 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 19 10:24:13 2011 +0200
@@ -124,7 +124,7 @@
                 | NONE => (Light, s))
   |> (fn (poly, (level, (heaviness, core))) =>
          case (core, (poly, level, heaviness)) of
-           ("simple_types", (NONE, _, Light)) => Simple_Types level
+           ("simple", (NONE, _, Light)) => Simple_Types level
          | ("preds", (SOME Polymorphic, _, _)) =>
            if level = All_Types then Preds (Polymorphic, level, heaviness)
            else raise Same.SAME