diff -r e6240d62a7e6 -r 90b2b2fd3fdf src/Pure/General/ROOT.ML
--- a/src/Pure/General/ROOT.ML	Mon Dec 12 15:37:35 2005 +0100
+++ b/src/Pure/General/ROOT.ML	Mon Dec 12 17:24:06 2005 +0100
@@ -15,6 +15,7 @@
 use "source.ML";
 use "symbol.ML";
 use "name_space.ML";
+use "name_mangler.ML";
 use "seq.ML";
 use "rat.ML";
 use "position.ML";