src/Pure/term.ML
changeset 39293 651e5a3e8cfd
parent 38980 af73cf0dc31f
child 40840 2f97215e79bf
     1.1 --- a/src/Pure/term.ML	Sun Sep 12 22:28:59 2010 +0200
     1.2 +++ b/src/Pure/term.ML	Mon Sep 13 00:10:29 2010 +0200
     1.3 @@ -420,7 +420,7 @@
     1.4      fun map_aux (Const (a, T)) = Const (a, f T)
     1.5        | map_aux (Free (a, T)) = Free (a, f T)
     1.6        | map_aux (Var (v, T)) = Var (v, f T)
     1.7 -      | map_aux (t as Bound _)  = t
     1.8 +      | map_aux (Bound i) = Bound i
     1.9        | map_aux (Abs (a, T, t)) = Abs (a, f T, map_aux t)
    1.10        | map_aux (t $ u) = map_aux t $ map_aux u;
    1.11    in map_aux end;