1.1 --- a/src/Tools/quickcheck.ML	Fri Mar 16 14:46:13 2012 +0100
     1.2 +++ b/src/Tools/quickcheck.ML	Fri Mar 16 18:20:12 2012 +0100
     1.3 @@ -83,7 +83,6 @@
     1.4  struct
     1.5  
     1.6  val quickcheckN = "quickcheck"
     1.7 -val quickcheck_paramsN = "quickcheck_params"
     1.8  
     1.9  val genuineN = "genuine"
    1.10  val noneN = "none"
    1.11 @@ -530,11 +529,12 @@
    1.12    @{keyword "["} |-- Parse.list1 parse_arg --| @{keyword "]"} || Scan.succeed [];
    1.13  
    1.14  val _ =
    1.15 -  Outer_Syntax.command quickcheck_paramsN "set parameters for random testing" Keyword.thy_decl
    1.16 +  Outer_Syntax.command @{command_spec "quickcheck_params"} "set parameters for random testing"
    1.17      (parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args)));
    1.18  
    1.19  val _ =
    1.20 -  Outer_Syntax.improper_command quickcheckN "try to find counterexample for subgoal" Keyword.diag
    1.21 +  Outer_Syntax.improper_command @{command_spec "quickcheck"}
    1.22 +    "try to find counterexample for subgoal"
    1.23      (parse_args -- Scan.optional Parse.nat 1
    1.24        >> (fn (args, i) => Toplevel.no_timing o Toplevel.keep (quickcheck_cmd args i)));
    1.25