# HG changeset patch
# User wenzelm
# Date 949697044 -3600
# Node ID 6483e7132a7052949b2642003466c7d6efa751dd
# Parent  626504b52668ca5742cd60b8558aa79a02605ca7
Present.old_symbol_source;

diff -r 626504b52668 -r 6483e7132a70 src/Pure/Isar/outer_syntax.ML
--- 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;