1.1 --- a/src/HOL/HOLCF/Tools/domaindef.ML	Thu Mar 15 19:48:19 2012 +0100
     1.2 +++ b/src/HOL/HOLCF/Tools/domaindef.ML	Thu Mar 15 20:07:00 2012 +0100
     1.3 @@ -212,13 +212,13 @@
     1.4  (** outer syntax **)
     1.5  
     1.6  val domaindef_decl =
     1.7 -  Scan.optional (Parse.$$$ "(" |--
     1.8 -      ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
     1.9 +  Scan.optional (@{keyword "("} |--
    1.10 +      ((@{keyword "open"} >> K false) -- Scan.option Parse.binding ||
    1.11          Parse.binding >> (fn s => (true, SOME s)))
    1.12 -        --| Parse.$$$ ")") (true, NONE) --
    1.13 +        --| @{keyword ")"}) (true, NONE) --
    1.14      (Parse.type_args_constrained -- Parse.binding) --
    1.15 -    Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.term) --
    1.16 -    Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding))
    1.17 +    Parse.opt_mixfix -- (@{keyword "="} |-- Parse.term) --
    1.18 +    Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
    1.19  
    1.20  fun mk_domaindef ((((((def, opt_name), (args, t)), mx), A), morphs)) =
    1.21    domaindef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs)