equal
deleted
inserted
replaced
198 val illegal_vars = |
198 val illegal_vars = |
199 if null (term_vars set) andalso null (term_tvars set) then [] |
199 if null (term_vars set) andalso null (term_tvars set) then [] |
200 else ["Illegal schematic variable(s) on rhs"]; |
200 else ["Illegal schematic variable(s) on rhs"]; |
201 |
201 |
202 val dup_lhs_tfrees = |
202 val dup_lhs_tfrees = |
203 (case duplicates lhs_tfrees of [] => [] |
203 (case gen_duplicates (op =) lhs_tfrees of [] => [] |
204 | dups => ["Duplicate type variables on lhs: " ^ show_names dups]); |
204 | dups => ["Duplicate type variables on lhs: " ^ show_names dups]); |
205 |
205 |
206 val extra_rhs_tfrees = |
206 val extra_rhs_tfrees = |
207 (case fold (remove (op =)) lhs_tfrees rhs_tfrees of [] => [] |
207 (case fold (remove (op =)) lhs_tfrees rhs_tfrees of [] => [] |
208 | extras => ["Extra type variables on rhs: " ^ show_names extras]); |
208 | extras => ["Extra type variables on rhs: " ^ show_names extras]); |