src/HOL/Library/refute.ML
changeset 59936 b8ffc3dc9e24
parent 59582 0fbed69ff081
child 60094 96a4765ba7d1
     1.1 --- a/src/HOL/Library/refute.ML	Mon Apr 06 16:30:44 2015 +0200
     1.2 +++ b/src/HOL/Library/refute.ML	Mon Apr 06 17:06:48 2015 +0200
     1.3 @@ -2965,7 +2965,7 @@
     1.4  (* 'refute' command *)
     1.5  
     1.6  val _ =
     1.7 -  Outer_Syntax.command @{command_spec "refute"}
     1.8 +  Outer_Syntax.command @{command_keyword refute}
     1.9      "try to find a model that refutes a given subgoal"
    1.10      (scan_parms -- Scan.optional Parse.nat 1 >>
    1.11        (fn (parms, i) =>
    1.12 @@ -2980,7 +2980,7 @@
    1.13  (* 'refute_params' command *)
    1.14  
    1.15  val _ =
    1.16 -  Outer_Syntax.command @{command_spec "refute_params"}
    1.17 +  Outer_Syntax.command @{command_keyword refute_params}
    1.18      "show/store default parameters for the 'refute' command"
    1.19      (scan_parms >> (fn parms =>
    1.20        Toplevel.theory (fn thy =>