changeset 6641 | 254ab03bd082 |
parent 6231 | 438a642ee92d |
child 7024 | 44bd3c094fd6 |
--- a/src/Pure/Thy/thy_syn.ML Wed May 12 16:52:28 1999 +0200 +++ b/src/Pure/Thy/thy_syn.ML Wed May 12 16:54:31 1999 +0200 @@ -55,7 +55,7 @@ val txt_out = ThyParse.parse_thy (! syntax) chs; in File.write tmp_path txt_out; - Symbol.use tmp_path; + File.symbol_use tmp_path; if ! delete_tmpfiles then File.rm tmp_path else () end;