1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Aug 22 12:16:56 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Aug 22 16:03:13 2013 +0200
     1.3 @@ -404,7 +404,7 @@
     1.4      else if subcommand = supported_proversN then
     1.5        supported_provers ctxt
     1.6      else if subcommand = kill_allN then
     1.7 -      (kill_provers (); kill_learners ())
     1.8 +      (kill_provers (); kill_learners ctxt)
     1.9      else if subcommand = running_proversN then
    1.10        running_provers ()
    1.11      else if subcommand = unlearnN then

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Aug 22 12:16:56 2013 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Aug 22 16:03:13 2013 +0200
     2.3 @@ -97,7 +97,7 @@
     2.4    val relevant_facts :
     2.5      Proof.context -> params -> string -> int -> fact_override -> term list
     2.6      -> term -> raw_fact list -> (string * fact list) list
     2.7 -  val kill_learners : unit -> unit
     2.8 +  val kill_learners : Proof.context -> unit
     2.9    val running_learners : unit -> unit
    2.10  end;
    2.11  
    2.12 @@ -253,10 +253,13 @@
    2.13  structure MaSh =
    2.14  struct
    2.15  
    2.16 +fun shutdown ctxt =
    2.17 +  run_mash_tool ctxt false [shutdown_server_arg] ([], K "") (K ())
    2.18 +
    2.19  fun unlearn ctxt =
    2.20    let val path = mash_model_dir () in
    2.21      trace_msg ctxt (K "MaSh unlearn");
    2.22 -    run_mash_tool ctxt false [shutdown_server_arg] ([], K "") (K ());
    2.23 +    shutdown ctxt;
    2.24      try (File.fold_dir (fn file => fn _ =>
    2.25                             try File.rm (Path.append path (Path.basic file)))
    2.26                         path) NONE;
    2.27 @@ -431,7 +434,7 @@
    2.28  fun clear_state ctxt =
    2.29    Synchronized.change global_state (fn _ =>
    2.30        (MaSh.unlearn ctxt; (* also removes the state file *)
    2.31 -       (true, empty_state)))
    2.32 +       (false, empty_state)))
    2.33  
    2.34  end
    2.35  
    2.36 @@ -1332,7 +1335,8 @@
    2.37        | _ => [("", mesh)]
    2.38      end
    2.39  
    2.40 -fun kill_learners () = Async_Manager.kill_threads MaShN "learner"
    2.41 +fun kill_learners ctxt =
    2.42 +  (Async_Manager.kill_threads MaShN "learner"; MaSh.shutdown ctxt)
    2.43  fun running_learners () = Async_Manager.running_threads MaShN "learner"
    2.44  
    2.45  end;