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