src/Pure/thm.ML
changeset 32035 8e77b6a250d5
parent 32032 a6a6e8031c14
child 32059 7991cdf10a54
     1.1 --- a/src/Pure/thm.ML	Fri Jul 17 22:54:11 2009 +0200
     1.2 +++ b/src/Pure/thm.ML	Fri Jul 17 23:11:40 2009 +0200
     1.3 @@ -317,7 +317,7 @@
     1.4        (Ctyp {T = TVar ((a, i), S), thy_ref = Theory.check_thy thy, maxidx = i, sorts = sorts},
     1.5         Ctyp {T = T, thy_ref = Theory.check_thy thy, maxidx = maxidx2, sorts = sorts});
     1.6      fun mk_ctinst ((x, i), (T, t)) =
     1.7 -      let val T = Envir.typ_subst_TVars Tinsts T in
     1.8 +      let val T = Envir.subst_type Tinsts T in
     1.9          (Cterm {t = Var ((x, i), T), T = T, thy_ref = Theory.check_thy thy,
    1.10            maxidx = i, sorts = sorts},
    1.11           Cterm {t = t, T = T, thy_ref = Theory.check_thy thy, maxidx = maxidx2, sorts = sorts})
    1.12 @@ -1467,7 +1467,7 @@
    1.13  fun norm_term_skip env 0 t = Envir.norm_term env t
    1.14    | norm_term_skip env n (Const ("all", _) $ Abs (a, T, t)) =
    1.15        let
    1.16 -        val T' = Envir.typ_subst_TVars (Envir.type_env env) T
    1.17 +        val T' = Envir.subst_type (Envir.type_env env) T
    1.18          (*Must instantiate types of parameters because they are flattened;
    1.19            this could be a NEW parameter*)
    1.20        in Term.all T' $ Abs (a, T', norm_term_skip env n t) end