src/HOLCF/Tools/adm_tac.ML
changeset 32035 8e77b6a250d5
parent 31023 d027411c9a38
child 33440 181fae134b43
     1.1 --- a/src/HOLCF/Tools/adm_tac.ML	Fri Jul 17 22:54:11 2009 +0200
     1.2 +++ b/src/HOLCF/Tools/adm_tac.ML	Fri Jul 17 23:11:40 2009 +0200
     1.3 @@ -117,8 +117,8 @@
     1.4      val tye' = Sign.typ_match thy (PT, #T (rep_cterm Pt)) tye;
     1.5      val ctye = map (fn (ixn, (S, T)) =>
     1.6        (ctyp_of thy (TVar (ixn, S)), ctyp_of thy T)) (Vartab.dest tye');
     1.7 -    val tv = cterm_of thy (Var (("t", j), Envir.typ_subst_TVars tye' tT));
     1.8 -    val Pv = cterm_of thy (Var (("P", j), Envir.typ_subst_TVars tye' PT));
     1.9 +    val tv = cterm_of thy (Var (("t", j), Envir.subst_type tye' tT));
    1.10 +    val Pv = cterm_of thy (Var (("P", j), Envir.subst_type tye' PT));
    1.11      val rule' = instantiate (ctye, [(tv, tt), (Pv, Pt)]) rule
    1.12    in rule' end;
    1.13