diff -r 309276732ee1 -r a233bc746c75 src/Pure/Interface/proof_general.ML
--- a/src/Pure/Interface/proof_general.ML	Fri Jul 09 16:54:54 1999 +0200
+++ b/src/Pure/Interface/proof_general.ML	Fri Jul 09 16:55:20 1999 +0200
@@ -7,7 +7,7 @@
 
 signature PROOF_GENERAL =
 sig
-  val write_keywords: string -> unit
+  val write_keywords: unit -> unit
   val setup: (theory -> theory) list
   val init: bool -> unit
 end;
@@ -41,10 +41,12 @@
   implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^
   "\n(provide 'isar-keywords)\n";
 
+val keywords_file = "isar-keywords.el";
+
 in
 
-fun write_keywords file =
-  File.write (Path.unpack file) (make_elisp_syntax (OuterSyntax.dest_syntax ()));
+fun write_keywords () =
+  File.write (Path.unpack keywords_file) (make_elisp_syntax (OuterSyntax.dest_syntax ()));
 
 end;