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