| changeset 12120 | a08c61932501 |
| parent 10252 | dd46544e259d |
| child 13533 | 70de987e9fe3 |
--- a/src/Pure/Thy/thy_load.ML Fri Nov 09 00:16:52 2001 +0100 +++ b/src/Pure/Thy/thy_load.ML Fri Nov 09 00:17:09 2001 +0100 @@ -88,7 +88,7 @@ fun load_file raw_path = (case check_file raw_path of None => error ("Could not find ML file " ^ quote (Path.pack raw_path)) - | Some (path, info) => (File.symbol_use path; (path, info))); + | Some (path, info) => (File.use path; (path, info))); (* datatype master *)