minor table access optimization

--- 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)