author | wenzelm |
Mon, 13 Sep 2010 00:10:29 +0200 | |
changeset 39293 | 651e5a3e8cfd |
parent 39292 | 6f085332c7d3 |
child 39294 | 27fae73fe769 |
src/Pure/term.ML | file | annotate | diff | comparison | revisions |
--- 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;