src/Pure/Syntax/ast.ML

--- a/src/Pure/Syntax/ast.ML	Tue Oct 20 13:37:56 2009 +0200
+++ b/src/Pure/Syntax/ast.ML	Tue Oct 20 16:13:01 2009 +0200
@@ -104,7 +104,7 @@
     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;