src/Pure/Thy/thy_syn.ML
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;