src/Pure/Isar/outer_syntax.ML
changeset 17283 881f5873bac0
parent 17265 12d99bb4304b
child 17412 e26cb20ef0cc
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Sep 06 16:59:57 2005 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Sep 06 16:59:58 2005 +0200
     1.3 @@ -278,7 +278,7 @@
     1.4      Present.init_theory name;
     1.5      Present.verbatim_source name present_text;
     1.6      if ThyHeader.is_old (text_src, pos) then
     1.7 -     (warning ("Non-Isar file format for theory " ^ quote name ^ " (deprecated)");
     1.8 +     (warning ("Non-Isar file format for theory " ^ quote name ^ " -- deprecated");
     1.9        ThySyn.load_thy name text;
    1.10        Present.old_symbol_source name present_text)   (*note: text presented twice*)
    1.11      else