# HG changeset patch
# User blanchet
# Date 1403614568 -7200
# Node ID cc2a820320580e34327202e3e9fc5f0da55f2475
# Parent  d2061dc953a46d44710ee18f6337b4ddea0f2dfa
minor table access optimization

diff -r d2061dc953a4 -r cc2a82032058 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Jun 24 13:48:14 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Jun 24 14:56:08 2014 +0200
@@ -497,7 +497,7 @@
         fun add_th weight t =
           let
             val im = Array.sub (sfreq, t)
-            fun fold_fn s sf = Inttab.update (s, weight + the_default 0 (Inttab.lookup im s)) sf
+            fun fold_fn s sf = Inttab.map_default (s, 0) (Integer.add weight) sf
           in
             Array.update (tfreq, t, weight + Array.sub (tfreq, t));
             Array.update (sfreq, t, fold fold_fn feats im)