# HG changeset patch
# User blanchet
# Date 1404059307 -7200
# Node ID 7e55bd4f9b0e6b7c2bb31fd1aa89f9cca8e1bab2
# Parent  78d7fbe9b20342c9415476467436c415495c1444
compile

diff -r 78d7fbe9b203 -r 7e55bd4f9b0e src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Sun Jun 29 18:28:27 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Sun Jun 29 18:28:27 2014 +0200
@@ -142,8 +142,7 @@
     if value <> ["false"] then
       param'
     else
-      error ("Parameter " ^ quote name ^ " cannot be set to \"false\" \
-             \(cf. " ^ quote name' ^ ").")
+      error ("Parameter " ^ quote name ^ " cannot be set to \"false\" (cf. " ^ quote name' ^ ").")
   | NONE =>
     (case AList.lookup (op =) negated_alias_params name of
       SOME name' => (name',
@@ -378,18 +377,15 @@
     else if subcommand = supported_proversN then
       supported_provers ctxt
     else if subcommand = kill_allN then
-      (kill_provers ();
-       kill_learners ctxt (get_params Normal thy override_params))
+      (kill_provers (); kill_learners ())
     else if subcommand = running_proversN then
       running_provers ()
     else if subcommand = unlearnN then
-      mash_unlearn ctxt (get_params Normal thy override_params)
+      mash_unlearn ()
     else if subcommand = learn_isarN orelse subcommand = learn_proverN orelse
             subcommand = relearn_isarN orelse subcommand = relearn_proverN then
-      (if subcommand = relearn_isarN orelse subcommand = relearn_proverN then
-         mash_unlearn ctxt (get_params Normal thy override_params)
-       else
-         ();
+      (if subcommand = relearn_isarN orelse subcommand = relearn_proverN then mash_unlearn ()
+       else ();
        mash_learn ctxt
            (* TODO: Use MaSh mode instead and have the special defaults hardcoded in "get_params" *)
            (get_params Normal thy
@@ -426,15 +422,14 @@
 val parse_value = Scan.repeat1 (Parse.xname || Parse.float_number || parse_query_bang)
 val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) []
 val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
-val parse_fact_refs =
-  Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse_Spec.xthm)
+val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse_Spec.xthm)
 val parse_fact_override_chunk =
   (Args.add |-- Args.colon |-- parse_fact_refs >> add_fact_override)
   || (Args.del |-- Args.colon |-- parse_fact_refs >> del_fact_override)
   || (parse_fact_refs >> only_fact_override)
 val parse_fact_override =
   Scan.optional (Args.parens (Scan.repeat parse_fact_override_chunk >> merge_fact_overrides))
-                no_fact_override
+    no_fact_override
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "sledgehammer"}