src/Pure/Isar/outer_syntax.ML

     val text_src = Source.of_list text;
     fun present_text () = Source.exhaust (Symbol.source false text_src);
   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
         val tok_src = text_src
           |> Symbol.source false