src/Pure/General/ROOT.ML
changeset 18387 90b2b2fd3fdf
parent 18132 0e9c9a18f454
child 20594 b80c4a5cd018
     1.1 --- a/src/Pure/General/ROOT.ML	Mon Dec 12 15:37:35 2005 +0100
     1.2 +++ b/src/Pure/General/ROOT.ML	Mon Dec 12 17:24:06 2005 +0100
     1.3 @@ -15,6 +15,7 @@
     1.4  use "source.ML";
     1.5  use "symbol.ML";
     1.6  use "name_space.ML";
     1.7 +use "name_mangler.ML";
     1.8  use "seq.ML";
     1.9  use "rat.ML";
    1.10  use "position.ML";