src/Pure/Pure.thy

--- a/src/Pure/Pure.thy	Tue Apr 05 15:27:11 2016 +0200
+++ b/src/Pure/Pure.thy	Tue Apr 05 15:53:48 2016 +0200
@@ -101,16 +101,16 @@
 local
 
 val _ =
-  Outer_Syntax.command ("ML_file", @{here}) "read and evaluate Isabelle/ML file"
+  Outer_Syntax.command @{command_keyword ML_file} "read and evaluate Isabelle/ML file"
     (Resources.parse_files "ML_file" >> ML_File.ML NONE);
 
 val _ =
-  Outer_Syntax.command ("ML_file_debug", @{here})
+  Outer_Syntax.command @{command_keyword ML_file_debug}
     "read and evaluate Isabelle/ML file (with debugger information)"
     (Resources.parse_files "ML_file_debug" >> ML_File.ML (SOME true));
 
 val _ =
-  Outer_Syntax.command ("ML_file_no_debug", @{here})
+  Outer_Syntax.command @{command_keyword ML_file_no_debug}
     "read and evaluate Isabelle/ML file (no debugger information)"
     (Resources.parse_files "ML_file_no_debug" >> ML_File.ML (SOME false));