Present.old_symbol_source;

--- a/src/Pure/Isar/outer_syntax.ML	Fri Feb 04 21:43:30 2000 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Feb 04 21:44:04 2000 +0100
@@ -403,7 +403,8 @@
   in
     Present.init_theory name;
     Present.verbatim_source name (present_text text);
-    if is_old_theory (src, pos) then ThySyn.load_thy name text
+    if is_old_theory (src, pos) then (ThySyn.load_thy name text;
+      Present.old_symbol_source name (present_text text))   (*note: text presented twice!*)
     else (Toplevel.excursion_error (parse_thy (src, pos));
       Present.token_source name (present_toks text pos))
   end;