# HG changeset patch
# User blanchet
# Date 1404226030 -7200
# Node ID b2bafc09b7e7fa2497fdd2d0f3ad1d8145b24c68
# Parent  eb55157849927fb5e34cdeaee2f725bdb6ee4638
clean up MaSh export a bit

diff -r eb5515784992 -r b2bafc09b7e7 src/HOL/TPTP/MaSh_Export.thy
--- a/src/HOL/TPTP/MaSh_Export.thy	Tue Jul 01 16:47:10 2014 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy	Tue Jul 01 16:47:10 2014 +0200
@@ -46,32 +46,74 @@
   ()
 *}
 
-ML {* Options.put_default @{system_option MaSh} "nb" *}
-
 ML {*
 if do_it then
-  generate_mash_suggestions @{context} params (range, step) thys max_suggestions
+  generate_mash_suggestions "nb" @{context} params (range, step) thys max_suggestions
     (prefix ^ "mash_nb_suggestions")
 else
   ()
 *}
 
-ML {* Options.put_default @{system_option MaSh} "knn" *}
-
 ML {*
 if do_it then
-  generate_mash_suggestions @{context} params (range, step) thys max_suggestions
+  generate_mash_suggestions "knn" @{context} params (range, step) thys max_suggestions
     (prefix ^ "mash_knn_suggestions")
 else
   ()
 *}
 
-ML {* Options.put_default @{system_option MaSh} "py" *}
+ML {*
+if do_it then
+  generate_mepo_suggestions @{context} params (range, step) thys max_suggestions
+    (prefix ^ "mepo_suggestions")
+else
+  ()
+*}
+
+ML {*
+if do_it then
+  generate_mesh_suggestions max_suggestions (prefix ^ "mash_nb_suggestions")
+    (prefix ^ "mepo_suggestions") (prefix ^ "mesh_nb_suggestions")
+else
+  ()
+*}
+
+ML {*
+if do_it then
+  generate_mesh_suggestions max_suggestions (prefix ^ "mash_knn_suggestions")
+    (prefix ^ "mepo_suggestions") (prefix ^ "mesh_knn_suggestions")
+else
+  ()
+*}
 
 ML {*
 if do_it then
-  generate_mash_suggestions @{context} params (range, step) thys max_suggestions
-    (prefix ^ "mash_py_suggestions")
+  generate_prover_dependencies @{context} params range thys
+    (prefix ^ "mash_nb_prover_dependencies")
+else
+  ()
+*}
+
+ML {*
+if do_it then
+  generate_prover_dependencies @{context} params range thys
+    (prefix ^ "mash_knn_prover_dependencies")
+else
+  ()
+*}
+
+ML {*
+if do_it then
+  generate_mesh_suggestions max_suggestions (prefix ^ "mash_nb_prover_suggestions")
+    (prefix ^ "mepo_suggestions") (prefix ^ "mesh_nb_prover_suggestions")
+else
+  ()
+*}
+
+ML {*
+if do_it then
+  generate_mesh_suggestions max_suggestions (prefix ^ "mash_knn_prover_suggestions")
+    (prefix ^ "mepo_suggestions") (prefix ^ "mesh_knn_prover_suggestions")
 else
   ()
 *}
@@ -107,41 +149,10 @@
 
 ML {*
 if do_it then
-  generate_mepo_suggestions @{context} params (range, step) thys max_suggestions
-    (prefix ^ "mepo_suggestions")
-else
-  ()
-*}
-
-ML {*
-if do_it then
-  generate_mesh_suggestions max_suggestions (prefix ^ "mash_suggestions")
-    (prefix ^ "mepo_suggestions") (prefix ^ "mesh_suggestions")
-else
-  ()
-*}
-
-ML {*
-if do_it then
-  generate_prover_dependencies @{context} params range thys (prefix ^ "mash_prover_dependencies")
-else
-  ()
-*}
-
-ML {*
-if do_it then
   generate_prover_commands @{context} params (range, step) thys max_suggestions
     (prefix ^ "mash_prover_commands")
 else
   ()
 *}
 
-ML {*
-if do_it then
-  generate_mesh_suggestions max_suggestions (prefix ^ "mash_prover_suggestions")
-    (prefix ^ "mepo_suggestions") (prefix ^ "mesh_prover_suggestions")
-else
-  ()
-*}
-
 end
diff -r eb5515784992 -r b2bafc09b7e7 src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Tue Jul 01 16:47:10 2014 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Tue Jul 01 16:47:10 2014 +0200
@@ -24,7 +24,7 @@
     theory list -> int -> string -> unit
   val generate_mepo_suggestions : Proof.context -> params -> (int * int option) * int ->
     theory list -> int -> string -> unit
-  val generate_mash_suggestions : Proof.context -> params -> (int * int option) * int ->
+  val generate_mash_suggestions : string -> Proof.context -> params -> (int * int option) * int ->
     theory list -> int -> string -> unit
   val generate_mesh_suggestions : int -> string -> string -> string -> unit
 end;
@@ -284,15 +284,16 @@
        not (Config.get ctxt Sledgehammer_MaSh.duplicates) ? Sledgehammer_Fact.drop_duplicate_facts
        #> Sledgehammer_MePo.mepo_suggested_facts ctxt params max_suggs NONE hyp_ts concl_t)
 
-fun generate_mash_suggestions ctxt params =
-  (Sledgehammer_MaSh.mash_unlearn ();
+fun generate_mash_suggestions engine =
+  (Options.put_default @{system_option MaSh} engine;
+   Sledgehammer_MaSh.mash_unlearn ();
    generate_mepo_or_mash_suggestions
      (fn ctxt => fn thy => fn params as {provers = prover :: _, ...} => fn max_suggs => fn hyp_ts =>
           fn concl_t =>
         tap (Sledgehammer_MaSh.mash_learn_facts ctxt params prover 2 false
           Sledgehammer_Util.one_year)
         #> Sledgehammer_MaSh.mash_suggested_facts ctxt thy params max_suggs hyp_ts concl_t
-        #> fst) ctxt params)
+        #> fst))
 
 fun generate_mesh_suggestions max_suggs mash_file_name mepo_file_name mesh_file_name =
   let