# HG changeset patch
# User blanchet
# Date 1401291756 -7200
# Node ID dc0b4f50e288831c9a1eaf14b604ab7fac6aa6fa
# Parent  2d502370ee9925a5cdcdd320bcab20f51a2fdaad
more generous max number of suggestions, for more safety

diff -r 2d502370ee99 -r dc0b4f50e288 src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Wed May 28 17:42:34 2014 +0200
+++ b/src/HOL/TPTP/mash_eval.ML	Wed May 28 17:42:36 2014 +0200
@@ -54,7 +54,7 @@
     fun print s = File.append report_path (s ^ "\n")
     val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} = default_params thy []
     val prover = hd provers
-    val slack_max_facts = generous_max_facts (the max_facts)
+    val max_suggs = generous_max_suggestions (the max_facts)
     val lines_of = Path.explode #> try File.read_lines #> these
     val file_names =
       [mepo_file_name, mash_isar_file_name, mash_prover_file_name,
@@ -97,7 +97,7 @@
                          mesh_isar_line), mesh_prover_line)) =
       if in_range range j then
         let
-          val get_suggs = extract_suggestions ##> take slack_max_facts
+          val get_suggs = extract_suggestions ##> take max_suggs
           val (name1, mepo_suggs) = get_suggs mepo_line
           val (name2, mash_isar_suggs) = get_suggs mash_isar_line
           val (name3, mash_prover_suggs) = get_suggs mash_prover_line
diff -r 2d502370ee99 -r dc0b4f50e288 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed May 28 17:42:34 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed May 28 17:42:36 2014 +0200
@@ -377,7 +377,9 @@
     val prop_tab = fold cons_thm facts Termtab.empty
     val plain_name_tab = Termtab.fold add_plains prop_tab Symtab.empty
     val inclass_name_tab = Symtab.fold add_inclass plain_name_tab Symtab.empty
-  in (plain_name_tab, inclass_name_tab) end
+  in
+    (plain_name_tab, inclass_name_tab)
+  end
 
 fun fact_distinct eq facts =
   fold (fn fact as (_, th) =>
diff -r 2d502370ee99 -r dc0b4f50e288 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed May 28 17:42:34 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed May 28 17:42:36 2014 +0200
@@ -85,7 +85,7 @@
   val mash_learn : Proof.context -> params -> fact_override -> thm list -> bool -> unit
 
   val mash_can_suggest_facts : Proof.context -> bool -> bool
-  val generous_max_facts : int -> int
+  val generous_max_suggestions : int -> int
   val mepo_weight : real
   val mash_weight : real
   val relevant_facts : Proof.context -> params -> string -> int -> fact_override -> term list ->
@@ -1574,7 +1574,7 @@
 
 (* Generate more suggestions than requested, because some might be thrown out
    later for various reasons. *)
-fun generous_max_facts max_facts = max_facts + Int.min (50, max_facts)
+fun generous_max_suggestions max_facts = max_facts (*### 11 * max_facts div 10 + 20 *)
 
 val mepo_weight = 0.5
 val mash_weight = 0.5
@@ -1655,7 +1655,7 @@
          |> weight_facts_steeply, [])
 
       fun mash () =
-        mash_suggested_facts ctxt params (generous_max_facts max_facts) hyp_ts concl_t facts
+        mash_suggested_facts ctxt params (generous_max_suggestions max_facts) hyp_ts concl_t facts
         |>> weight_facts_steeply
 
       val mess =
diff -r 2d502370ee99 -r dc0b4f50e288 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed May 28 17:42:34 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed May 28 17:42:36 2014 +0200
@@ -84,9 +84,8 @@
 fun reserved_isar_keyword_table () =
   Keyword.dest () |-> union (op =) |> map (rpair ()) |> Symtab.make
 
-(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few
-   fixes that seem to be missing over there; or maybe the two code portions are
-   not doing the same? *)
+(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few fixes that seem to
+   be missing over there; or maybe the two code portions are not doing the same? *)
 fun fold_body_thm outer_name (map_plain_name, map_inclass_name) =
   let
     fun app_thm map_name (_, (name, _, body)) accum =
@@ -104,7 +103,9 @@
           accum |> union (op =) (the_list (map_name name))
       end
     and app_body map_name (PBody {thms, ...}) = fold (app_thm map_name) thms
-  in app_body map_plain_name end
+  in
+    app_body map_plain_name
+  end
 
 fun thms_in_proof name_tabs th =
   let val map_names = (case name_tabs of SOME p => pairself Symtab.lookup p | NONE => `I SOME) in