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