Present.old_symbol_source;
authorwenzelm
Fri Feb 04 21:44:04 2000 +0100 (2000-02-04)
changeset 81916483e7132a70
parent 8190 626504b52668
child 8192 45a7027136e3
Present.old_symbol_source;
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Fri Feb 04 21:43:30 2000 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Fri Feb 04 21:44:04 2000 +0100
     1.3 @@ -403,7 +403,8 @@
     1.4    in
     1.5      Present.init_theory name;
     1.6      Present.verbatim_source name (present_text text);
     1.7 -    if is_old_theory (src, pos) then ThySyn.load_thy name text
     1.8 +    if is_old_theory (src, pos) then (ThySyn.load_thy name text;
     1.9 +      Present.old_symbol_source name (present_text text))   (*note: text presented twice!*)
    1.10      else (Toplevel.excursion_error (parse_thy (src, pos));
    1.11        Present.token_source name (present_toks text pos))
    1.12    end;