src/Pure/Isar/outer_keyword.ML
changeset 27768 398c64b2acef
parent 27526 69618a03b6f7
child 27805 2e533bcd1343
     1.1 --- a/src/Pure/Isar/outer_keyword.ML	Thu Aug 07 13:44:56 2008 +0200
     1.2 +++ b/src/Pure/Isar/outer_keyword.ML	Thu Aug 07 13:45:03 2008 +0200
     1.3 @@ -154,11 +154,11 @@
     1.4  (* augment tables *)
     1.5  
     1.6  fun keyword name =
     1.7 - (change_lexicons (apfst (Scan.extend_lexicon [Symbol.explode name]));
     1.8 + (change_lexicons (apfst (Scan.extend_lexicon (Symbol.explode name)));
     1.9    Pretty.writeln (report_keyword name));
    1.10  
    1.11  fun command name kind =
    1.12 - (change_lexicons (apsnd (Scan.extend_lexicon [Symbol.explode name]));
    1.13 + (change_lexicons (apsnd (Scan.extend_lexicon (Symbol.explode name)));
    1.14    change_commands (Symtab.update (name, kind));
    1.15    Pretty.writeln (report_command (name, kind)));
    1.16