# HG changeset patch
# User wenzelm
# Date 1127948342 -7200
# Node ID 299eeb303f049ed7e9fedea31541695cf107625b
# Parent  6c6ecafd8c0ea661e27a4322f0ca379429b61515
tuned default operation: use internal modify;

diff -r 6c6ecafd8c0e -r 299eeb303f04 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Thu Sep 29 00:59:01 2005 +0200
+++ b/src/Pure/General/table.ML	Thu Sep 29 00:59:02 2005 +0200
@@ -104,7 +104,7 @@
           fold right (f p2 (fold mid (f p1 (fold left x))));
   in fold end;
 
-fun fold_map_table f = 
+fun fold_map_table f =
   let
     fun fold_map Empty s = (Empty, s)
       | fold_map (Branch2 (left, p as (k, x), right)) s =
@@ -224,7 +224,7 @@
 
 fun update (key, x) tab = modify key (fn _ => x) tab;
 fun update_new (key, x) tab = modify key (fn NONE => x | SOME _ => raise DUP key) tab;
-fun default (p as (key, x)) tab = if defined tab key then tab else update p tab;
+fun default (key, x) tab = modify key (fn NONE => x | SOME _ => raise SAME) tab;
 fun map_entry key f = modify key (fn NONE => raise SAME | SOME x => f x);