src/Pure/pattern.ML
changeset 33037 b22e44496dc2
parent 32738 15bb09ca0378
child 33038 8f9594c31de4
     1.1 --- a/src/Pure/pattern.ML	Tue Oct 20 13:37:56 2009 +0200
     1.2 +++ b/src/Pure/pattern.ML	Tue Oct 20 16:13:01 2009 +0200
     1.3 @@ -216,10 +216,10 @@
     1.4  
     1.5  fun flexflex2(env,binders,F,Fty,is,G,Gty,js) =
     1.6    let fun ff(F,Fty,is,G as (a,_),Gty,js) =
     1.7 -            if js subset_int is
     1.8 +            if gen_subset (op =) (js, is)
     1.9              then let val t= mkabs(binders,is,app(Var(G,Gty),map (idx is) js))
    1.10                   in Envir.update (((F, Fty), t), env) end
    1.11 -            else let val ks = is inter_int js
    1.12 +            else let val ks = gen_inter (op =) (is, js)
    1.13                       val Hty = type_of_G env (Fty,length is,map (idx is) ks)
    1.14                       val (env',H) = Envir.genvar a (env,Hty)
    1.15                       fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks));
    1.16 @@ -339,7 +339,7 @@
    1.17    let val js = loose_bnos t
    1.18    in if null is
    1.19       then if null js then Vartab.update_new (ixn, (T, t)) itms else raise MATCH
    1.20 -     else if js subset_int is
    1.21 +     else if gen_subset (op =) (js, is)
    1.22            then let val t' = if downto0(is,length binders - 1) then t
    1.23                              else mapbnd (idx is) t
    1.24                 in Vartab.update_new (ixn, (T, mkabs (binders, is, t'))) itms end