src/Pure/Pure.thy
changeset 62867 cce0570d1bfa
parent 62862 007c454d0d0f
child 62873 2f9c8a18f832
     1.1 --- a/src/Pure/Pure.thy	Tue Apr 05 15:27:11 2016 +0200
     1.2 +++ b/src/Pure/Pure.thy	Tue Apr 05 15:53:48 2016 +0200
     1.3 @@ -101,16 +101,16 @@
     1.4  local
     1.5  
     1.6  val _ =
     1.7 -  Outer_Syntax.command ("ML_file", @{here}) "read and evaluate Isabelle/ML file"
     1.8 +  Outer_Syntax.command @{command_keyword ML_file} "read and evaluate Isabelle/ML file"
     1.9      (Resources.parse_files "ML_file" >> ML_File.ML NONE);
    1.10  
    1.11  val _ =
    1.12 -  Outer_Syntax.command ("ML_file_debug", @{here})
    1.13 +  Outer_Syntax.command @{command_keyword ML_file_debug}
    1.14      "read and evaluate Isabelle/ML file (with debugger information)"
    1.15      (Resources.parse_files "ML_file_debug" >> ML_File.ML (SOME true));
    1.16  
    1.17  val _ =
    1.18 -  Outer_Syntax.command ("ML_file_no_debug", @{here})
    1.19 +  Outer_Syntax.command @{command_keyword ML_file_no_debug}
    1.20      "read and evaluate Isabelle/ML file (no debugger information)"
    1.21      (Resources.parse_files "ML_file_no_debug" >> ML_File.ML (SOME false));
    1.22