src/Pure/term.ML
changeset 32784 1a5dde5079ac
parent 32738 15bb09ca0378
child 33063 4d462963a7db
     1.1 --- a/src/Pure/term.ML	Wed Sep 30 19:04:48 2009 +0200
     1.2 +++ b/src/Pure/term.ML	Wed Sep 30 22:20:58 2009 +0200
     1.3 @@ -796,7 +796,7 @@
     1.4        let
     1.5          fun subst (Const (a, T)) = Const (a, typ_subst_TVars instT T)
     1.6            | subst (Free (a, T)) = Free (a, typ_subst_TVars instT T)
     1.7 -          | subst (t as Var (xi, T)) =
     1.8 +          | subst (Var (xi, T)) =
     1.9                (case AList.lookup (op =) inst xi of
    1.10                  NONE => Var (xi, typ_subst_TVars instT T)
    1.11                | SOME t => t)