changeset 5864 | 30b6a3251813 |
parent 5040 | 78abd4c4802a |
child 6116 | 8ba2f25610f7 |
--- a/src/Pure/General/ROOT.ML Sat Nov 14 13:25:34 1998 +0100 +++ b/src/Pure/General/ROOT.ML Sat Nov 14 13:26:11 1998 +0100 @@ -12,3 +12,15 @@ use "path.ML"; use "file.ML"; use "history.ML"; + +structure PureGeneral = +struct + structure Symtab = Symtab; + structure Object = Object; + structure Seq = Seq; + structure NameSpace = NameSpace; + structure Position = Position; + structure Path = Path; + structure File = File; + structure History = History; +end;