# HG changeset patch
# User wenzelm
# Date 916690362 -3600
# Node ID 166b3353aad5735b637c852f92aa378ccd8f679b
# Parent  cf917037cfd462cc97bdab5c0c9948475b0e4e6f
structure Graph = Graph;

diff -r cf917037cfd4 -r 166b3353aad5 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;