src/HOL/SMT_Examples/boogie.ML

--- a/src/HOL/SMT_Examples/boogie.ML	Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/SMT_Examples/boogie.ML	Mon Apr 06 17:06:48 2015 +0200
@@ -266,7 +266,7 @@
 (* Isar command *)
 
 val _ =
-  Outer_Syntax.command @{command_spec "boogie_file"}
+  Outer_Syntax.command @{command_keyword boogie_file}
     "prove verification condition from .b2i file"
     (Resources.provide_parse_files "boogie_file" >> (fn files =>
       Toplevel.theory (fn thy =>