diff -r aae5566d6756 -r 94aa7b81bcf6 src/HOL/Tools/Quickcheck/abstract_generators.ML
--- 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)))