equal
deleted
inserted
replaced
129 |
129 |
130 fun add_sort_env (Type (_, Ts), env) = foldr add_sort_env (Ts, env) |
130 fun add_sort_env (Type (_, Ts), env) = foldr add_sort_env (Ts, env) |
131 | add_sort_env (TFree (x, S), env) = ins_entry (S, x) env |
131 | add_sort_env (TFree (x, S), env) = ins_entry (S, x) env |
132 | add_sort_env (TVar (xi, S), env) = ins_entry (S, string_of_vname xi) env; |
132 | add_sort_env (TVar (xi, S), env) = ins_entry (S, string_of_vname xi) env; |
133 |
133 |
134 val sort = map (apsnd sort_strings); |
134 fun sort l = map (apsnd sort_strings) l; |
135 in |
135 in |
136 fun type_env t = sort (add_type_env (t, [])); |
136 fun type_env t = sort (add_type_env (t, [])); |
137 fun sort_env t = rev (sort (it_term_types add_sort_env (t, []))); |
137 fun sort_env t = rev (sort (it_term_types add_sort_env (t, []))); |
138 end; |
138 end; |
139 |
139 |