# HG changeset patch
# User blanchet
# Date 1403782539 -7200
# Node ID b89937ed60992ceb015ae337de038f843893aa30
# Parent  e64c1b174f4bd999016a80d8e321d0749c8f318c
tuning

diff -r e64c1b174f4b -r b89937ed6099 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Jun 26 13:35:36 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Jun 26 13:35:39 2014 +0200
@@ -206,7 +206,7 @@
       |> map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts)
       |> space_implode "\n\n")
 
-fun run_sledgehammer (params as {debug, verbose, spy, blocking, provers, max_facts, ...}) mode
+fun run_sledgehammer (params as {verbose, spy, blocking, provers, max_facts, ...}) mode
     output_result i (fact_override as {only, ...}) minimize_command state =
   if null provers then
     error "No prover is set."
diff -r e64c1b174f4b -r b89937ed6099 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jun 26 13:35:36 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jun 26 13:35:39 2014 +0200
@@ -145,6 +145,8 @@
 val relearn_isarN = "relearn_isar"
 val relearn_proverN = "relearn_prover"
 
+fun map_array_at ary f i = Array.update (ary, i, f (Array.sub (ary, i)))
+
 fun mash_state_dir () = Path.explode "$ISABELLE_HOME_USER/mash" |> tap Isabelle_System.mkdir
 fun mash_state_file () = Path.append (mash_state_dir ()) (Path.explode "state")
 
@@ -418,7 +420,7 @@
   let
     val dffreq = Array.array (num_feats, 0)
 
-    fun add_sym s = Array.update (dffreq, s, 1 + Array.sub (dffreq, s))
+    val add_sym = map_array_at dffreq (Integer.add 1)
     fun for1 i =
       if i = num_feats then () else
       (List.app (fn _ => add_sym i) (get_sym_ths i); for1 (i + 1))
@@ -499,11 +501,11 @@
             val im = Array.sub (sfreq, t)
             fun fold_fn s sf = Inttab.map_default (s, 0) (Integer.add weight) sf
           in
-            Array.update (tfreq, t, weight + Array.sub (tfreq, t));
+            map_array_at tfreq (Integer.add weight) t;
             Array.update (sfreq, t, fold fold_fn feats im)
           end
 
-        fun add_sym s = Array.update (dffreq, s, 1 + Array.sub (dffreq, s))
+        val add_sym = map_array_at dffreq (Integer.add 1)
       in
         add_th nb_def_prior_weight th;
         List.app (add_th 1) deps;
@@ -634,8 +636,6 @@
 fun add_to_xtab key (next, tab) = (next + 1, Symtab.update_new (key, next) tab)
 fun maybe_add_to_xtab key = perhaps (try (add_to_xtab key))
 
-fun map_array_at ary f i = Array.update (ary, i, f (Array.sub (ary, i)))
-
 fun query ctxt overlord engine visible_facts max_suggs (learns0, hints, feats) =
   let
     val learns = learns0 @ (if null hints then [] else [(".hints", feats, hints)])