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