src/Pure/Syntax/ast.ML
changeset 33038 8f9594c31de4
parent 33037 b22e44496dc2
child 33955 fff6f11b1f09
equal deleted inserted replaced
33037:b22e44496dc2 33038:8f9594c31de4
   102 
   102 
   103     val lvars = add_vars lhs [];
   103     val lvars = add_vars lhs [];
   104     val rvars = add_vars rhs [];
   104     val rvars = add_vars rhs [];
   105   in
   105   in
   106     if has_duplicates (op =) lvars then SOME "duplicate vars in lhs"
   106     if has_duplicates (op =) lvars then SOME "duplicate vars in lhs"
   107     else if not (gen_subset (op =) (rvars, lvars)) then SOME "rhs contains extra variables"
   107     else if not (subset (op =) (rvars, lvars)) then SOME "rhs contains extra variables"
   108     else NONE
   108     else NONE
   109   end;
   109   end;
   110 
   110 
   111 
   111 
   112 
   112