src/Pure/Thy/thy_parse.ML
changeset 4056 abb0f4742ed7
parent 4047 67b5552b1067
child 4099 0ec0d2dbe3f4
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Fri Oct 31 15:21:59 1997 +0100
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Fri Oct 31 15:28:01 1997 +0100
     1.3 @@ -437,9 +437,14 @@
     1.4    lexicon * (token list -> (string * string) * token list) Symtab.table;
     1.5  
     1.6  fun make_syntax keywords sects =
     1.7 -  (make_lexicon (map fst sects @ keywords),
     1.8 -    Symtab.make sects handle Symtab.DUPS dups =>
     1.9 -      error ("Duplicate sections in theory file syntax: " ^ commas_quote dups));
    1.10 +  let
    1.11 +    val dups = duplicates (map fst sects);
    1.12 +    val sects' = gen_distinct eq_fst sects;
    1.13 +  in
    1.14 +    if null dups then ()
    1.15 +    else warning ("Duplicate declaration of theory file sections:\n" ^ commas_quote dups);
    1.16 +    (make_lexicon (map fst sects' @ keywords), Symtab.make sects')
    1.17 +  end;
    1.18  
    1.19  
    1.20  (* header *)
    1.21 @@ -511,6 +516,7 @@
    1.22      \|> Theory.add_name " ^ quote thy_name ^ ";\n\
    1.23      \\n\
    1.24      \val _ = store_theory (thy, " ^ quote thy_name ^ ");\n\
    1.25 +    \val _ = context thy;\n\
    1.26      \\n\
    1.27      \\n"
    1.28      ^ postxt ^ "\n\