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