# HG changeset patch
# User wenzelm
# Date 1284329429 -7200
# Node ID 651e5a3e8cfd8773e6cb0a67b6580d74ce87e2ac
# Parent  6f085332c7d3281b77a4967d22536209e436688f
tuned;

diff -r 6f085332c7d3 -r 651e5a3e8cfd src/Pure/term.ML
--- 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;