--- a/src/Pure/Isar/outer_syntax.ML Fri Sep 02 21:29:55 2005 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Sat Sep 03 16:44:17 2005 +0200
@@ -278,7 +278,9 @@
in
Present.init_theory name;
Present.verbatim_source name present_text;
- if ThyHeader.is_old (text_src, pos) then (ThySyn.load_thy name text;
+ if ThyHeader.is_old (text_src, pos) then
+ (warning ("Non-Isar file format for theory " ^ quote name ^ " -- deprecated!");
+ ThySyn.load_thy name text;
Present.old_symbol_source name present_text) (*note: text presented twice*)
else
let