src/Pure/Isar/outer_syntax.ML
changeset 17237 75407a6f02d2
parent 17221 6cd180204582
child 17250 158ef530c153
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Fri Sep 02 21:29:55 2005 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sat Sep 03 16:44:17 2005 +0200
     1.3 @@ -278,7 +278,9 @@
     1.4    in
     1.5      Present.init_theory name;
     1.6      Present.verbatim_source name present_text;
     1.7 -    if ThyHeader.is_old (text_src, pos) then (ThySyn.load_thy name text;
     1.8 +    if ThyHeader.is_old (text_src, pos) then
     1.9 +     (warning ("Non-Isar file format for theory " ^ quote name ^ " -- deprecated!");
    1.10 +      ThySyn.load_thy name text;
    1.11        Present.old_symbol_source name present_text)   (*note: text presented twice*)
    1.12      else
    1.13        let