changeset 39293 | 651e5a3e8cfd |
parent 38980 | af73cf0dc31f |
child 40840 | 2f97215e79bf |
--- 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;