changeset 33038 | 8f9594c31de4 |
parent 33037 | b22e44496dc2 |
child 33955 | fff6f11b1f09 |
--- 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;