--- 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 *)
--- 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