src/Pure/pattern.ML
changeset 33049 c38f02fdf35d
parent 33038 8f9594c31de4
child 35210 6e45e4c94751
     1.1 --- a/src/Pure/pattern.ML	Wed Oct 21 10:15:31 2009 +0200
     1.2 +++ b/src/Pure/pattern.ML	Wed Oct 21 12:09:37 2009 +0200
     1.3 @@ -219,7 +219,7 @@
     1.4              if subset (op =) (js, is)
     1.5              then let val t= mkabs(binders,is,app(Var(G,Gty),map (idx is) js))
     1.6                   in Envir.update (((F, Fty), t), env) end
     1.7 -            else let val ks = inter (op =) (is, js)
     1.8 +            else let val ks = inter (op =) js is
     1.9                       val Hty = type_of_G env (Fty,length is,map (idx is) ks)
    1.10                       val (env',H) = Envir.genvar a (env,Hty)
    1.11                       fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks));