src/Pure/meta_simplifier.ML

 (*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 gen_subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) then uncond_skel args
   else skel0;
 
 (*
   Rewriting -- we try in order:
     (1) beta reduction