src/Pure/ROOT.ML
changeset 38448 62d16c415019
parent 38418 9a7af64d71bb
child 38470 484e483eb606
     1.1 --- a/src/Pure/ROOT.ML	Mon Aug 16 22:56:28 2010 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Tue Aug 17 15:10:49 2010 +0200
     1.3 @@ -42,6 +42,7 @@
     1.4  use "General/ord_list.ML";
     1.5  use "General/balanced_tree.ML";
     1.6  use "General/graph.ML";
     1.7 +use "General/linear_set.ML";
     1.8  use "General/long_name.ML";
     1.9  use "General/binding.ML";
    1.10  use "General/name_space.ML";