structure Graph = Graph;
authorwenzelm
Mon, 18 Jan 1999 21:12:42 +0100
changeset 6136 166b3353aad5
parent 6135 cf917037cfd4
child 6137 5cb525437aab
structure Graph = Graph;
src/Pure/General/ROOT.ML
--- a/src/Pure/General/ROOT.ML	Mon Jan 18 21:09:34 1999 +0100
+++ b/src/Pure/General/ROOT.ML	Mon Jan 18 21:12:42 1999 +0100
@@ -21,6 +21,7 @@
 structure PureGeneral =
 struct
   structure Symtab = Symtab;
+  structure Graph = Graph;
   structure Object = Object;
   structure Seq = Seq;
   structure NameSpace = NameSpace;