changeset 6231 | 438a642ee92d |
parent 6206 | 7d2204fcc1e5 |
child 6641 | 254ab03bd082 |
--- a/src/Pure/Thy/thy_syn.ML Thu Feb 04 18:17:01 1999 +0100 +++ b/src/Pure/Thy/thy_syn.ML Thu Feb 04 18:17:20 1999 +0100 @@ -55,7 +55,7 @@ val txt_out = ThyParse.parse_thy (! syntax) chs; in File.write tmp_path txt_out; - Use.use_path tmp_path; + Symbol.use tmp_path; if ! delete_tmpfiles then File.rm tmp_path else () end;