src/HOL/Tools/refute.ML
changeset 46961 5c6955f487e5
parent 46960 f19e5837ad69
child 48902 44a6967240b7
     1.1 --- a/src/HOL/Tools/refute.ML	Fri Mar 16 14:46:13 2012 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Fri Mar 16 18:20:12 2012 +0100
     1.3 @@ -3198,8 +3198,8 @@
     1.4  (* 'refute' command *)
     1.5  
     1.6  val _ =
     1.7 -  Outer_Syntax.improper_command "refute"
     1.8 -    "try to find a model that refutes a given subgoal" Keyword.diag
     1.9 +  Outer_Syntax.improper_command @{command_spec "refute"}
    1.10 +    "try to find a model that refutes a given subgoal"
    1.11      (scan_parms -- Scan.optional Parse.nat 1 >>
    1.12        (fn (parms, i) =>
    1.13          Toplevel.keep (fn state =>
    1.14 @@ -3212,8 +3212,8 @@
    1.15  (* 'refute_params' command *)
    1.16  
    1.17  val _ =
    1.18 -  Outer_Syntax.command "refute_params"
    1.19 -    "show/store default parameters for the 'refute' command" Keyword.thy_decl
    1.20 +  Outer_Syntax.command @{command_spec "refute_params"}
    1.21 +    "show/store default parameters for the 'refute' command"
    1.22      (scan_parms >> (fn parms =>
    1.23        Toplevel.theory (fn thy =>
    1.24          let