src/Pure/Syntax/ast.ML

 
     val lvars = add_vars lhs [];
     val rvars = add_vars rhs [];
   in
     if has_duplicates (op =) lvars then SOME "duplicate vars in lhs"
-    else if not (rvars subset lvars) then SOME "rhs contains extra variables"
+    else if not (gen_subset (op =) (rvars, lvars)) then SOME "rhs contains extra variables"
     else NONE
   end;