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";