1.1 --- a/src/HOL/Tools/choice_specification.ML	Thu Mar 15 19:48:19 2012 +0100
     1.2 +++ b/src/HOL/Tools/choice_specification.ML	Thu Mar 15 20:07:00 2012 +0100
     1.3 @@ -234,11 +234,11 @@
     1.4  
     1.5  (* outer syntax *)
     1.6  
     1.7 -val opt_name = Scan.optional (Parse.name --| Parse.$$$ ":") ""
     1.8 +val opt_name = Scan.optional (Parse.name --| @{keyword ":"}) ""
     1.9  val opt_overloaded = Parse.opt_keyword "overloaded"
    1.10  
    1.11  val specification_decl =
    1.12 -  Parse.$$$ "(" |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| Parse.$$$ ")" --
    1.13 +  @{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} --
    1.14            Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop)
    1.15  
    1.16  val _ =
    1.17 @@ -249,7 +249,7 @@
    1.18  
    1.19  val ax_specification_decl =
    1.20      Parse.name --
    1.21 -    (Parse.$$$ "(" |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| Parse.$$$ ")" --
    1.22 +    (@{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} --
    1.23             Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop))
    1.24  
    1.25  val _ =