42 use "General/same.ML"; |
42 use "General/same.ML"; |
43 use "General/ord_list.ML"; |
43 use "General/ord_list.ML"; |
44 use "General/balanced_tree.ML"; |
44 use "General/balanced_tree.ML"; |
45 use "General/graph.ML"; |
45 use "General/graph.ML"; |
46 use "General/linear_set.ML"; |
46 use "General/linear_set.ML"; |
47 use "General/long_name.ML"; |
|
48 use "General/binding.ML"; |
|
49 use "General/path.ML"; |
47 use "General/path.ML"; |
50 use "General/url.ML"; |
48 use "General/url.ML"; |
51 use "General/buffer.ML"; |
49 use "General/buffer.ML"; |
52 use "General/file.ML"; |
50 use "General/file.ML"; |
53 use "General/xml.ML"; |
51 use "General/xml.ML"; |
54 use "General/xml_data.ML"; |
52 use "General/xml_data.ML"; |
55 use "General/yxml.ML"; |
53 use "General/yxml.ML"; |
56 use "General/pretty.ML"; |
54 use "General/pretty.ML"; |
|
55 use "General/long_name.ML"; |
|
56 use "General/binding.ML"; |
57 |
57 |
58 use "General/sha1.ML"; |
58 use "General/sha1.ML"; |
59 if String.isPrefix "polyml" ml_system |
59 if String.isPrefix "polyml" ml_system |
60 then use "General/sha1_polyml.ML" |
60 then use "General/sha1_polyml.ML" |
61 else (); |
61 else (); |