src/Tools/Code/code_runtime.ML
changeset 59936 b8ffc3dc9e24
parent 59633 a372513af1e2
child 60956 10d463883dc2
     1.1 --- a/src/Tools/Code/code_runtime.ML	Mon Apr 06 16:30:44 2015 +0200
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Mon Apr 06 17:06:48 2015 +0200
     1.3 @@ -475,7 +475,7 @@
     1.4  in
     1.5  
     1.6  val _ =
     1.7 -  Outer_Syntax.command @{command_spec "code_reflect"}
     1.8 +  Outer_Syntax.command @{command_keyword code_reflect}
     1.9      "enrich runtime environment with generated code"
    1.10      (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- Parse.!!!  (parse_datatype
    1.11        ::: Scan.repeat (@{keyword "and"} |-- parse_datatype))) []