1.1 --- a/src/Pure/Interface/proof_general.ML	Fri Jul 16 22:26:44 1999 +0200
     1.2 +++ b/src/Pure/Interface/proof_general.ML	Fri Jul 16 22:27:16 1999 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4    "\n  '(" ^ space_implode "\n    " (map (quote o regexp_quote) strs) ^ "))\n";
     1.5  
     1.6  fun make_elisp_commands commands kind =
     1.7 -  defconst kind (mapfilter (fn (c, k) => if k = kind then Some c else None) commands);
     1.8 +  defconst kind (mapfilter (fn (c, _, k, _) => if k = kind then Some c else None) commands);
     1.9  
    1.10  fun make_elisp_syntax (keywords, commands) =
    1.11    ";;\n\
    1.12 @@ -37,7 +37,7 @@
    1.13    \;;\n\
    1.14    \;; $" ^ "Id$\n\
    1.15    \;;\n" ^
    1.16 -  defconst "minor" (filter Syntax.is_identifier (keywords \\ map #1 commands)) ^
    1.17 +  defconst "minor" (filter Syntax.is_identifier keywords) ^
    1.18    implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^
    1.19    "\n(provide 'isar-keywords)\n";
    1.20  
    1.21 @@ -46,7 +46,8 @@
    1.22  in
    1.23  
    1.24  fun write_keywords () =
    1.25 -  File.write (Path.unpack keywords_file) (make_elisp_syntax (OuterSyntax.dest_syntax ()));
    1.26 +  File.write (Path.unpack keywords_file)
    1.27 +    (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ()));
    1.28  
    1.29  end;
    1.30