equal
deleted
inserted
replaced
19 use "pretty.ML"; |
19 use "pretty.ML"; |
20 |
20 |
21 structure PureGeneral = |
21 structure PureGeneral = |
22 struct |
22 struct |
23 structure Symtab = Symtab; |
23 structure Symtab = Symtab; |
|
24 structure Graph = Graph; |
24 structure Object = Object; |
25 structure Object = Object; |
25 structure Seq = Seq; |
26 structure Seq = Seq; |
26 structure NameSpace = NameSpace; |
27 structure NameSpace = NameSpace; |
27 structure Position = Position; |
28 structure Position = Position; |
28 structure Path = Path; |
29 structure Path = Path; |