structure Graph = Graph;
authorwenzelm
Mon Jan 18 21:12:42 1999 +0100 (1999-01-18)
changeset 6136166b3353aad5
parent 6135 cf917037cfd4
child 6137 5cb525437aab
structure Graph = Graph;
src/Pure/General/ROOT.ML
     1.1 --- a/src/Pure/General/ROOT.ML	Mon Jan 18 21:09:34 1999 +0100
     1.2 +++ b/src/Pure/General/ROOT.ML	Mon Jan 18 21:12:42 1999 +0100
     1.3 @@ -21,6 +21,7 @@
     1.4  structure PureGeneral =
     1.5  struct
     1.6    structure Symtab = Symtab;
     1.7 +  structure Graph = Graph;
     1.8    structure Object = Object;
     1.9    structure Seq = Seq;
    1.10    structure NameSpace = NameSpace;