src/Pure/pattern.ML

   else let val ks = mk_ff_list(is,js)
        in mknewhnf(env,binders,is,F,Fty,ks) end;
 
 fun flexflex2(env,binders,F,Fty,is,G,Gty,js) =
   let fun ff(F,Fty,is,G as (a,_),Gty,js) =
-            if gen_subset (op =) (js, is)
+            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 = gen_inter (op =) (is, js)
+            else let val ks = inter (op =) (is, js)
                      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));
                  in Envir.update (((G, Gty), lam js), Envir.update (((F, Fty), lam is), env'))
                  end;

 
 fun match_bind(itms,binders,ixn,T,is,t) =
   let val js = loose_bnos t
   in if null is
      then if null js then Vartab.update_new (ixn, (T, t)) itms else raise MATCH
-     else if gen_subset (op =) (js, is)
+     else if subset (op =) (js, is)
           then let val t' = if downto0(is,length binders - 1) then t
                             else mapbnd (idx is) t
                in Vartab.update_new (ixn, (T, mkabs (binders, is, t'))) itms end
           else raise MATCH
   end;