# HG changeset patch
# User wenzelm
# Date 1125758657 -7200
# Node ID 75407a6f02d25e5d36067c0c8e6dcd9f1edbd18f
# Parent  6edb84c661dd51b7ebc75f30d79160f6c1ebee6b
deprecated non-Isar theory file format;

diff -r 6edb84c661dd -r 75407a6f02d2 src/Pure/Isar/outer_syntax.ML
--- 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