# HG changeset patch
# User wenzelm
# Date 1218136077 -7200
# Node ID cd5ae3dbd30e66b24c0bd1d6da14575648b5c901
# Parent  377810fd718e887fa5e50dc34c1ac22047f0c013
map_default: more explicit scope;

diff -r 377810fd718e -r cd5ae3dbd30e src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Thu Aug 07 21:07:55 2008 +0200
+++ b/src/Pure/General/table.ML	Thu Aug 07 21:07:57 2008 +0200
@@ -250,7 +250,7 @@
 fun update_new (key, x) tab = modify key (fn NONE => x | SOME _ => raise DUP key) 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);
-fun map_default (key, x) f = modify key (fn NONE => f x | SOME x => f x);
+fun map_default (key, x) f = modify key (fn NONE => f x | SOME y => f y);
 
 
 (* delete *)