# HG changeset patch
# User blanchet
# Date 1401273266 -7200
# Node ID c881a983a19fa50c397a93ea8688d16eec0302aa
# Parent  28618ccec4c77d526fe0237fc98310d1104fbd80
optimized computation

diff -r 28618ccec4c7 -r c881a983a19f src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed May 28 10:04:28 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed May 28 12:34:26 2014 +0200
@@ -192,8 +192,7 @@
 val auto_try_max_facts_divisor = 2 (* FUDGE *)
 
 fun string_of_facts facts =
-  "Including " ^ string_of_int (length facts) ^
-  " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
+  "Including " ^ string_of_int (length facts) ^ " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
   (facts |> map (fst o fst) |> space_implode " ") ^ "."
 
 fun string_of_factss factss =
diff -r 28618ccec4c7 -r c881a983a19f src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed May 28 10:04:28 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed May 28 12:34:26 2014 +0200
@@ -437,19 +437,19 @@
 
     fun learn th syms deps =
       let
-        fun add_th t =
+        fun add_th weight t =
           let
             val im = Array.sub (sfreq, t)
-            fun fold_fn s sf = Inttab.update (s, 1 + the_default 0 (Inttab.lookup im s)) sf
+            fun fold_fn s sf = Inttab.update (s, weight + the_default 0 (Inttab.lookup im s)) sf
           in
-            Array.update (tfreq, t, 1 + Array.sub (tfreq, t));
+            Array.update (tfreq, t, weight + Array.sub (tfreq, t));
             Array.update (sfreq, t, fold fold_fn syms im)
           end
 
         fun add_sym s = Array.update (dffreq, s, 1 + Array.sub (dffreq, s))
       in
-        List.app add_th (replicate nb_def_prior_weight th);
-        List.app add_th deps;
+        add_th nb_def_prior_weight th;
+        List.app (add_th 1) deps;
         List.app add_sym syms;
         afreq := !afreq + 1
       end