src/HOL/Library/code_test.ML
changeset 59936 b8ffc3dc9e24
parent 59720 f893472fff31
child 60022 ea987317a785
     1.1 --- a/src/HOL/Library/code_test.ML	Mon Apr 06 16:30:44 2015 +0200
     1.2 +++ b/src/HOL/Library/code_test.ML	Mon Apr 06 17:06:48 2015 +0200
     1.3 @@ -567,7 +567,7 @@
     1.4  val test_codeP = Scan.repeat1 Parse.prop -- (@{keyword "in"} |-- Scan.repeat1 Parse.name)
     1.5  
     1.6  val _ = 
     1.7 -  Outer_Syntax.command @{command_spec "test_code"}
     1.8 +  Outer_Syntax.command @{command_keyword test_code}
     1.9      "compile test cases to target languages, execute them and report results"
    1.10        (test_codeP >> (fn (raw_ts, targets) => Toplevel.keep (test_code_cmd raw_ts targets)))
    1.11