src/Pure/meta_simplifier.ML

   | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
   | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
   | vperm (t, u) = (t = u);
 
 fun var_perm (t, u) =
-  vperm (t, u) andalso gen_eq_set (op =) (Term.add_vars t [], Term.add_vars u []);
+  vperm (t, u) andalso eq_set (op =) (Term.add_vars t [], Term.add_vars u []);
 
 (*simple test for looping rewrite rules and stupid orientations*)
 fun default_reorient thy prems lhs rhs =
   rewrite_rule_extra_vars prems lhs rhs
     orelse

 (*Behaves like unconditional rule if rhs does not contain vars not in the lhs.
   Otherwise those vars may become instantiated with unnormalized terms
   while the premises are solved.*)
 
 fun cond_skel (args as (_, (lhs, rhs))) =
-  if Term.add_vars rhs [] subset Term.add_vars lhs [] then uncond_skel args
+  if subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) then uncond_skel args
   else skel0;
 
 (*
   Rewriting -- we try in order:
     (1) beta reduction