equal
deleted
inserted
replaced
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 |