src/HOL/SMT_Examples/boogie.ML
changeset 59936 b8ffc3dc9e24
parent 58061 3d060f43accb
child 61424 c3658c18b7bc
     1.1 --- a/src/HOL/SMT_Examples/boogie.ML	Mon Apr 06 16:30:44 2015 +0200
     1.2 +++ b/src/HOL/SMT_Examples/boogie.ML	Mon Apr 06 17:06:48 2015 +0200
     1.3 @@ -266,7 +266,7 @@
     1.4  (* Isar command *)
     1.5  
     1.6  val _ =
     1.7 -  Outer_Syntax.command @{command_spec "boogie_file"}
     1.8 +  Outer_Syntax.command @{command_keyword boogie_file}
     1.9      "prove verification condition from .b2i file"
    1.10      (Resources.provide_parse_files "boogie_file" >> (fn files =>
    1.11        Toplevel.theory (fn thy =>