diff -r b22e44496dc2 -r 8f9594c31de4 src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Tue Oct 20 16:13:01 2009 +0200
+++ b/src/Pure/Syntax/ast.ML	Wed Oct 21 08:14:38 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 (gen_subset (op =) (rvars, lvars)) then SOME "rhs contains extra variables"
+    else if not (subset (op =) (rvars, lvars)) then SOME "rhs contains extra variables"
     else NONE
   end;