--- a/src/HOL/Tools/Quickcheck/abstract_generators.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML Thu Mar 15 20:07:00 2012 +0100
@@ -66,8 +66,8 @@
val _ = Outer_Syntax.command "quickcheck_generator" "define quickcheck generators for abstract types"
Keyword.thy_decl ((Parse.type_const --
- Scan.option (Args.$$$ "predicate" |-- Parse.$$$ ":" |-- Parse.term)) --
- (Args.$$$ "constructors" |-- Parse.$$$ ":" |-- Parse.list1 Parse.term)
+ Scan.option (Args.$$$ "predicate" |-- @{keyword ":"} |-- Parse.term)) --
+ (Args.$$$ "constructors" |-- @{keyword ":"} |-- Parse.list1 Parse.term)
>> (fn ((tyco, opt_pred), constrs) =>
Toplevel.theory (quickcheck_generator_cmd tyco opt_pred constrs)))