# HG changeset patch
# User wenzelm
# Date 1459864428 -7200
# Node ID cce0570d1bfa23382e0d574eefe2249edecb2de1
# Parent  d20262cd20e89e727cd5d81f00b98c6b19efd317
tuned;

diff -r d20262cd20e8 -r cce0570d1bfa 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));