src/Pure/proofterm.ML
changeset 32035 8e77b6a250d5
parent 32032 a6a6e8031c14
child 32049 d6065a237059
     1.1 --- a/src/Pure/proofterm.ML	Fri Jul 17 22:54:11 2009 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Fri Jul 17 23:11:40 2009 +0200
     1.3 @@ -1087,7 +1087,7 @@
     1.4  
     1.5  fun prf_subst (pinst, (tyinsts, insts)) =
     1.6    let
     1.7 -    val substT = Envir.typ_subst_TVars tyinsts;
     1.8 +    val substT = Envir.subst_type tyinsts;
     1.9  
    1.10      fun subst' lev (t as Var (ixn, _)) = (case AList.lookup (op =) insts ixn of
    1.11            NONE => t