src/Pure/Syntax/ast.ML
changeset 33037 b22e44496dc2
parent 32784 1a5dde5079ac
child 33038 8f9594c31de4
     1.1 --- a/src/Pure/Syntax/ast.ML	Tue Oct 20 13:37:56 2009 +0200
     1.2 +++ b/src/Pure/Syntax/ast.ML	Tue Oct 20 16:13:01 2009 +0200
     1.3 @@ -104,7 +104,7 @@
     1.4      val rvars = add_vars rhs [];
     1.5    in
     1.6      if has_duplicates (op =) lvars then SOME "duplicate vars in lhs"
     1.7 -    else if not (rvars subset lvars) then SOME "rhs contains extra variables"
     1.8 +    else if not (gen_subset (op =) (rvars, lvars)) then SOME "rhs contains extra variables"
     1.9      else NONE
    1.10    end;
    1.11