# HG changeset patch
# User wenzelm
# Date 878308081 -3600
# Node ID abb0f4742ed7b8888d959aafbb49bc9bf7c48abe
# Parent  69892b85f800aea6905319b45419aa6933ca1e6a
dup sections: warning instead of error;

diff -r 69892b85f800 -r abb0f4742ed7 src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Fri Oct 31 15:21:59 1997 +0100
+++ b/src/Pure/Thy/thy_parse.ML	Fri Oct 31 15:28:01 1997 +0100
@@ -437,9 +437,14 @@
   lexicon * (token list -> (string * string) * token list) Symtab.table;
 
 fun make_syntax keywords sects =
-  (make_lexicon (map fst sects @ keywords),
-    Symtab.make sects handle Symtab.DUPS dups =>
-      error ("Duplicate sections in theory file syntax: " ^ commas_quote dups));
+  let
+    val dups = duplicates (map fst sects);
+    val sects' = gen_distinct eq_fst sects;
+  in
+    if null dups then ()
+    else warning ("Duplicate declaration of theory file sections:\n" ^ commas_quote dups);
+    (make_lexicon (map fst sects' @ keywords), Symtab.make sects')
+  end;
 
 
 (* header *)
@@ -511,6 +516,7 @@
     \|> Theory.add_name " ^ quote thy_name ^ ";\n\
     \\n\
     \val _ = store_theory (thy, " ^ quote thy_name ^ ");\n\
+    \val _ = context thy;\n\
     \\n\
     \\n"
     ^ postxt ^ "\n\