src/HOL/Boogie/Tools/boogie_commands.ML

 
 val vc_offsets = Scan.optional (Args.bracks (Parse.list1
   (Parse.string --| Args.colon -- Parse.nat))) []
 
 val _ =
-  Outer_Syntax.command "boogie_open"
+  Outer_Syntax.command @{command_spec "boogie_open"}
     "open a new Boogie environment and load a Boogie-generated .b2i file"
-    Keyword.thy_decl
     (scan_opt "quiet" -- Parse.name -- vc_offsets >> 
       (Toplevel.theory o boogie_open))
 
 
 val vc_name = Parse.name

     scan_val "only" vc_labels >> VC_Only ||
     scan_val "without" vc_labels >> VC_Without) ||
   Scan.succeed VC_Complete
 
 val _ =
-  Outer_Syntax.command "boogie_vc"
+  Outer_Syntax.command @{command_spec "boogie_vc"}
     "enter into proof mode for a specific verification condition"
-    Keyword.thy_goal
     (vc_name -- vc_opts >> (fn args =>
       (Toplevel.print o Toplevel.theory_to_proof (boogie_vc args))))
 
 
 val quick_timeout = 5

 
 fun status_cmd f = Toplevel.no_timing o Toplevel.keep (fn state =>
   f (Toplevel.theory_of state))
 
 val _ =
-  Outer_Syntax.improper_command "boogie_status"
+  Outer_Syntax.improper_command @{command_spec "boogie_status"}
     "show the name and state of all loaded verification conditions"
-    Keyword.diag
     (status_test >> status_cmd ||
      status_vc >> status_cmd ||
      Scan.succeed (status_cmd boogie_status))
 
 
 val _ =
-  Outer_Syntax.command "boogie_end"
+  Outer_Syntax.command @{command_spec "boogie_end"}
     "close the current Boogie environment"
-    Keyword.thy_decl
     (Scan.succeed (Toplevel.theory boogie_end))
 
 
 val setup = Theory.at_end (fn thy =>
   let