equal
deleted
inserted
replaced
224 end; |
224 end; |
225 |
225 |
226 structure Basic_Term_Ord: BASIC_TERM_ORD = TermOrd; |
226 structure Basic_Term_Ord: BASIC_TERM_ORD = TermOrd; |
227 open Basic_Term_Ord; |
227 open Basic_Term_Ord; |
228 |
228 |
229 |
229 structure Var_Graph = Graph(type key = indexname val ord = TermOrd.fast_indexname_ord); |
|
230 structure Sort_Graph = Graph(type key = sort val ord = TermOrd.sort_ord); |
|
231 structure Typ_Graph = Graph(type key = typ val ord = TermOrd.typ_ord); |
230 structure Term_Graph = Graph(type key = term val ord = TermOrd.fast_term_ord); |
232 structure Term_Graph = Graph(type key = term val ord = TermOrd.fast_term_ord); |
231 |
233 |