src/Pure/Thy/thy_parse.ML

 
 type syntax =
   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 *)
 
 fun mk_header (thy_name, bases) =

     ^ extxt ^ "\n\
     \\n\
     \|> Theory.add_name " ^ quote thy_name ^ ";\n\
     \\n\
     \val _ = store_theory (thy, " ^ quote thy_name ^ ");\n\
+    \val _ = context thy;\n\
     \\n\
     \\n"
     ^ postxt ^ "\n\
     \\n\
     \end;\n\