diff -r e194213451c9 -r 34f080a12063 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jun 11 17:07:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jun 11 17:10:23 2010 +0200
@@ -345,8 +345,8 @@
                               >> merge_relevance_overrides))
                 (add_to_relevance_override [])
 val parse_sledgehammer_command =
-  (Scan.optional Parse.short_ident runN -- parse_params -- parse_relevance_override
-   -- Scan.option Parse.nat) #>> sledgehammer_trans
+  (Scan.optional Parse.short_ident runN -- parse_params
+   -- parse_relevance_override -- Scan.option Parse.nat) #>> sledgehammer_trans
 val parse_sledgehammer_params_command =
   parse_params #>> sledgehammer_params_trans