1.1 --- a/src/Pure/Thy/thy_parse.ML	Mon Mar 09 16:14:32 1998 +0100
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Mon Mar 09 16:14:46 1998 +0100
     1.3 @@ -431,16 +431,17 @@
     1.4  (** theory syntax **)
     1.5  
     1.6  type syntax =
     1.7 -  lexicon * (token list -> (string * string) * token list) Symtab.table;
     1.8 +  Scan.lexicon * (token list -> (string * string) * token list) Symtab.table;
     1.9  
    1.10  fun make_syntax keywords sects =
    1.11    let
    1.12      val dups = duplicates (map fst sects);
    1.13      val sects' = gen_distinct eq_fst sects;
    1.14 +    val keys = map Symbol.explode (map fst sects' @ keywords);
    1.15    in
    1.16      if null dups then ()
    1.17      else warning ("Duplicate declaration of theory file sections:\n" ^ commas_quote dups);
    1.18 -    (make_lexicon (map fst sects' @ keywords), Symtab.make sects')
    1.19 +    (Scan.make_lexicon keys, Symtab.make sects')
    1.20    end;
    1.21  
    1.22  
    1.23 @@ -474,7 +475,7 @@
    1.24    | sect _ [] = eof_err ();
    1.25  
    1.26  fun extension sectab = "+" $$-- !!
    1.27 -  (repeat (sect sectab) --$$ "end" -- optional ("ML" $$-- verbatim) "")
    1.28 +  (repeat (sect sectab) --$$ "end" -- optional verbatim "")
    1.29      >> mk_extension;
    1.30  
    1.31  fun opt_extension sectab = optional (extension sectab) ("", "", "");