tuned;

--- a/src/Pure/term.ML	Sun Sep 12 22:28:59 2010 +0200
+++ b/src/Pure/term.ML	Mon Sep 13 00:10:29 2010 +0200
@@ -420,7 +420,7 @@
     fun map_aux (Const (a, T)) = Const (a, f T)
       | map_aux (Free (a, T)) = Free (a, f T)
       | map_aux (Var (v, T)) = Var (v, f T)
-      | map_aux (t as Bound _)  = t
+      | map_aux (Bound i) = Bound i
       | map_aux (Abs (a, T, t)) = Abs (a, f T, map_aux t)
       | map_aux (t $ u) = map_aux t $ map_aux u;
   in map_aux end;