removed warn_theory_style;
authorwenzelm
Mon, 16 Aug 1999 16:44:47 +0200
changeset 7212 1ad29e7d917b
parent 7211 8e4aa9044599
child 7213 08a354bbc34c
removed warn_theory_style;
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;