1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Mar 16 14:46:13 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Mar 16 18:20:12 2012 +0100
     1.3 @@ -413,20 +413,16 @@
     1.4    Scan.optional (Args.parens (Scan.repeat parse_relevance_chunk
     1.5                                >> merge_relevance_overrides))
     1.6                  no_relevance_override
     1.7 -val parse_sledgehammer_command =
     1.8 -  (Scan.optional Parse.short_ident runN -- parse_params
     1.9 -   -- parse_relevance_override -- Scan.option Parse.nat) #>> sledgehammer_trans
    1.10 -val parse_sledgehammer_params_command =
    1.11 -  parse_params #>> sledgehammer_params_trans
    1.12  
    1.13  val _ =
    1.14 -  Outer_Syntax.improper_command sledgehammerN
    1.15 -      "search for first-order proof using automatic theorem provers" Keyword.diag
    1.16 -      parse_sledgehammer_command
    1.17 +  Outer_Syntax.improper_command @{command_spec "sledgehammer"}
    1.18 +    "search for first-order proof using automatic theorem provers"
    1.19 +    ((Scan.optional Parse.short_ident runN -- parse_params
    1.20 +      -- parse_relevance_override -- Scan.option Parse.nat) #>> sledgehammer_trans)
    1.21  val _ =
    1.22 -  Outer_Syntax.command sledgehammer_paramsN
    1.23 -      "set and display the default parameters for Sledgehammer" Keyword.thy_decl
    1.24 -      parse_sledgehammer_params_command
    1.25 +  Outer_Syntax.command @{command_spec "sledgehammer_params"}
    1.26 +    "set and display the default parameters for Sledgehammer"
    1.27 +    (parse_params #>> sledgehammer_params_trans)
    1.28  
    1.29  fun try_sledgehammer auto state =
    1.30    let