equal
deleted
inserted
replaced
135 val lhs_dups = duplicates args; |
135 val lhs_dups = duplicates args; |
136 val rhs_extras = gen_rems (op =) (term_frees rhs, args); |
136 val rhs_extras = gen_rems (op =) (term_frees rhs, args); |
137 val rhs_extrasT = gen_rems (op =) (term_tfrees rhs, typ_tfrees ty); |
137 val rhs_extrasT = gen_rems (op =) (term_tfrees rhs, typ_tfrees ty); |
138 in |
138 in |
139 if not (forall is_Free args) then |
139 if not (forall is_Free args) then |
140 err "Arguments of lhs have to be variables" |
140 err "Arguments (on lhs) must be variables" |
141 else if not (null lhs_dups) then |
141 else if not (null lhs_dups) then |
142 err ("Duplicate variables on lhs: " ^ show_frees lhs_dups) |
142 err ("Duplicate variables on lhs: " ^ show_frees lhs_dups) |
143 else if not (null rhs_extras) then |
143 else if not (null rhs_extras) then |
144 err ("Extra variables on rhs: " ^ show_frees rhs_extras) |
144 err ("Extra variables on rhs: " ^ show_frees rhs_extras) |
145 else if not (null rhs_extrasT) then |
145 else if not (null rhs_extrasT) then |