# HG changeset patch
# User blanchet
# Date 1379709570 -7200
# Node ID be91786f2419538930960145b79157da27c25b60
# Parent  b8e62805566b3f2e07fcb3079d12eb7292b7734e
MaSh tweaks to facilitate debugging

diff -r b8e62805566b -r be91786f2419 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Sep 20 20:21:54 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Sep 20 22:39:30 2013 +0200
@@ -262,7 +262,7 @@
 
 fun shutdown ctxt overlord =
   (trace_msg ctxt (K "MaSh shutdown");
-   run_mash_tool ctxt overlord [shutdown_server_arg] true ([], K "") (K ()))
+   run_mash_tool ctxt overlord [shutdown_server_arg] false ([], K "") (K ()))
 
 fun save ctxt overlord =
   (trace_msg ctxt (K "MaSh save");
@@ -1229,14 +1229,15 @@
       end
   end
 
-fun mash_learn ctxt (params as {provers, timeout, ...}) fact_override chained
-               run_prover =
+fun mash_learn ctxt (params as {provers, timeout, max_facts, ...}) fact_override
+               chained run_prover =
   let
     val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
     val ctxt = ctxt |> Config.put instantiate_inducts false
     val facts =
       nearly_all_facts ctxt false fact_override Symtab.empty css chained []
                        @{prop True}
+      |> (case max_facts of NONE => I | SOME n => take n)
     val num_facts = length facts
     val prover = hd provers
     fun learn auto_level run_prover =