--- a/src/HOL/Library/refute.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Library/refute.ML Mon Apr 06 17:06:48 2015 +0200
@@ -2965,7 +2965,7 @@
(* 'refute' command *)
val _ =
- Outer_Syntax.command @{command_spec "refute"}
+ Outer_Syntax.command @{command_keyword refute}
"try to find a model that refutes a given subgoal"
(scan_parms -- Scan.optional Parse.nat 1 >>
(fn (parms, i) =>
@@ -2980,7 +2980,7 @@
(* 'refute_params' command *)
val _ =
- Outer_Syntax.command @{command_spec "refute_params"}
+ Outer_Syntax.command @{command_keyword refute_params}
"show/store default parameters for the 'refute' command"
(scan_parms >> (fn parms =>
Toplevel.theory (fn thy =>