# HG changeset patch
# User wenzelm
# Date 934814687 -7200
# Node ID 1ad29e7d917bb9460bb665f0c166441c27ef8eff
# Parent  8e4aa9044599ac08448f5ca05f6761cd473e8a33
removed warn_theory_style;

diff -r 8e4aa9044599 -r 1ad29e7d917b src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Mon Aug 16 16:44:24 1999 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Aug 16 16:44:47 1999 +0200
@@ -236,12 +236,6 @@
 fun is_old_theory src =
   is_none (scan_header (K check_header_lexicon) (Scan.option theory_keyword) src);
 
-fun warn_theory_style path is_old =
-  let
-    val style = if is_old then "old" else "new";
-    val _ = warning ("Assuming " ^ style ^ "-style theory format for " ^ quote (Path.pack path));
-  in is_old end;
-
 
 (* deps_thy --- inspect theory header *)
 
@@ -273,10 +267,9 @@
 fun deps_thy name path =
   let
     val src = File.source path;
-    val is_old = warn_theory_style path (is_old_theory src);
     val (name', parents, files) =
       (*Note: old style headers dynamically depend on the current lexicon :-( *)
-      if is_old then scan_header ThySyn.get_lexicon (Scan.error old_header) src
+      if is_old_theory src then scan_header ThySyn.get_lexicon (Scan.error old_header) src
       else scan_header (K header_lexicon) (Scan.error new_header) src;
 
     val ml_path = ThyLoad.ml_path name;