diff -r d2e8342bf5c3 -r 254ab03bd082 src/Pure/Thy/thy_syn.ML
--- 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;