# HG changeset patch
# User wenzelm
# Date 932156836 -7200
# Node ID ca0fbe679bbbd50a8cf82132d02299a7152522d0
# Parent  69724548fad154211c1f66026fb0c99ff40ce2aa
adapted to dest_keywords, dest_parsers;

diff -r 69724548fad1 -r ca0fbe679bbb src/Pure/Interface/proof_general.ML
--- a/src/Pure/Interface/proof_general.ML	Fri Jul 16 22:26:44 1999 +0200
+++ b/src/Pure/Interface/proof_general.ML	Fri Jul 16 22:27:16 1999 +0200
@@ -28,7 +28,7 @@
   "\n  '(" ^ space_implode "\n    " (map (quote o regexp_quote) strs) ^ "))\n";
 
 fun make_elisp_commands commands kind =
-  defconst kind (mapfilter (fn (c, k) => if k = kind then Some c else None) commands);
+  defconst kind (mapfilter (fn (c, _, k, _) => if k = kind then Some c else None) commands);
 
 fun make_elisp_syntax (keywords, commands) =
   ";;\n\
@@ -37,7 +37,7 @@
   \;;\n\
   \;; $" ^ "Id$\n\
   \;;\n" ^
-  defconst "minor" (filter Syntax.is_identifier (keywords \\ map #1 commands)) ^
+  defconst "minor" (filter Syntax.is_identifier keywords) ^
   implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^
   "\n(provide 'isar-keywords)\n";
 
@@ -46,7 +46,8 @@
 in
 
 fun write_keywords () =
-  File.write (Path.unpack keywords_file) (make_elisp_syntax (OuterSyntax.dest_syntax ()));
+  File.write (Path.unpack keywords_file)
+    (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ()));
 
 end;