# HG changeset patch
# User wenzelm
# Date 1431090447 -7200
# Node ID 3bb094031275f6d80418996a2766619abdbcc9b5
# Parent  d8a4fe35da00740eef7804bf1489f7976663d463
more standard command setup;

diff -r d8a4fe35da00 -r 3bb094031275 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri May 08 14:40:34 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri May 08 15:07:27 2015 +0200
@@ -358,19 +358,9 @@
       error ("Unknown subcommand: " ^ quote subcommand ^ ".")
   end
 
-fun sledgehammer_trans (((subcommand, params), fact_override), opt_i) =
-  Toplevel.keep_proof (hammer_away params subcommand opt_i fact_override o Toplevel.proof_of)
-
 fun string_of_raw_param (key, values) =
   key ^ (case implode_param values of "" => "" | value => " = " ^ value)
 
-fun sledgehammer_params_trans params =
-  Toplevel.theory (fold set_default_raw_param params #> tap (fn thy =>
-    writeln ("Default parameters for Sledgehammer:\n" ^
-      (case rev (default_raw_params Normal thy) of
-        [] => "none"
-      | params => params |> map string_of_raw_param |> sort_strings |> cat_lines))))
-
 val parse_query_bang = @{keyword "?"} || @{keyword "!"} || @{keyword "!!"}
 val parse_key = Scan.repeat1 (Parse.typ_group || parse_query_bang) >> implode_param
 val parse_value = Scan.repeat1 (Parse.xname || Parse.float_number || parse_query_bang)
@@ -389,11 +379,18 @@
   Outer_Syntax.command @{command_keyword sledgehammer}
     "search for first-order proof using automatic theorem provers"
     ((Scan.optional Parse.name runN -- parse_params
-      -- parse_fact_override -- Scan.option Parse.nat) #>> sledgehammer_trans)
+      -- parse_fact_override -- Scan.option Parse.nat) >>
+      (fn (((subcommand, params), fact_override), opt_i) =>
+        Toplevel.keep_proof (hammer_away params subcommand opt_i fact_override o Toplevel.proof_of)))
 val _ =
   Outer_Syntax.command @{command_keyword sledgehammer_params}
     "set and display the default parameters for Sledgehammer"
-    (parse_params #>> sledgehammer_params_trans)
+    (parse_params >> (fn params =>
+      Toplevel.theory (fold set_default_raw_param params #> tap (fn thy =>
+        writeln ("Default parameters for Sledgehammer:\n" ^
+          (case rev (default_raw_params Normal thy) of
+            [] => "none"
+          | params => params |> map string_of_raw_param |> sort_strings |> cat_lines))))))
 
 fun try_sledgehammer auto state =
   let