diff -r 85fc589a66ea -r 438a642ee92d src/Pure/Thy/thy_syn.ML
--- 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;