1.1 --- a/src/HOL/HOLCF/Tools/Domain/domain.ML	Thu Mar 15 19:48:19 2012 +0100
     1.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain.ML	Thu Mar 15 20:07:00 2012 +0100
     1.3 @@ -229,21 +229,21 @@
     1.4  (** outer syntax **)
     1.5  
     1.6  val dest_decl : (bool * binding option * string) parser =
     1.7 -  Parse.$$$ "(" |-- Scan.optional (Parse.$$$ "lazy" >> K true) false --
     1.8 -    (Parse.binding >> SOME) -- (Parse.$$$ "::" |-- Parse.typ)  --| Parse.$$$ ")" >> Parse.triple1
     1.9 -    || Parse.$$$ "(" |-- Parse.$$$ "lazy" |-- Parse.typ --| Parse.$$$ ")"
    1.10 -    >> (fn t => (true,NONE,t))
    1.11 -    || Parse.typ >> (fn t => (false,NONE,t))
    1.12 +  @{keyword "("} |-- Scan.optional (@{keyword "lazy"} >> K true) false --
    1.13 +    (Parse.binding >> SOME) -- (@{keyword "::"} |-- Parse.typ)  --| @{keyword ")"} >> Parse.triple1
    1.14 +    || @{keyword "("} |-- @{keyword "lazy"} |-- Parse.typ --| @{keyword ")"}
    1.15 +    >> (fn t => (true, NONE, t))
    1.16 +    || Parse.typ >> (fn t => (false, NONE, t))
    1.17  
    1.18  val cons_decl =
    1.19    Parse.binding -- Scan.repeat dest_decl -- Parse.opt_mixfix
    1.20  
    1.21  val domain_decl =
    1.22    (Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix) --
    1.23 -    (Parse.$$$ "=" |-- Parse.enum1 "|" cons_decl)
    1.24 +    (@{keyword "="} |-- Parse.enum1 "|" cons_decl)
    1.25  
    1.26  val domains_decl =
    1.27 -  Scan.optional (Parse.$$$ "(" |-- (Parse.$$$ "unsafe" >> K true) --| Parse.$$$ ")") false --
    1.28 +  Scan.optional (@{keyword "("} |-- (@{keyword "unsafe"} >> K true) --| @{keyword ")"}) false --
    1.29      Parse.and_list1 domain_decl
    1.30  
    1.31  fun mk_domain

     2.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Thu Mar 15 19:48:19 2012 +0100
     2.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Thu Mar 15 20:07:00 2012 +0100
     2.3 @@ -762,8 +762,8 @@
     2.4  val parse_domain_iso :
     2.5      (string list * binding * mixfix * string * (binding * binding) option)
     2.6        parser =
     2.7 -  (Parse.type_args -- Parse.binding -- Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) --
     2.8 -    Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding)))
     2.9 +  (Parse.type_args -- Parse.binding -- Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --
    2.10 +    Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)))
    2.11      >> (fn ((((vs, t), mx), rhs), morphs) => (vs, t, mx, rhs, morphs))
    2.12  
    2.13  val parse_domain_isos = Parse.and_list1 parse_domain_iso

     3.1 --- a/src/HOL/HOLCF/Tools/cpodef.ML	Thu Mar 15 19:48:19 2012 +0100
     3.2 +++ b/src/HOL/HOLCF/Tools/cpodef.ML	Thu Mar 15 20:07:00 2012 +0100
     3.3 @@ -344,13 +344,13 @@
     3.4  (** outer syntax **)
     3.5  
     3.6  val typedef_proof_decl =
     3.7 -  Scan.optional (Parse.$$$ "(" |--
     3.8 -      ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
     3.9 +  Scan.optional (@{keyword "("} |--
    3.10 +      ((@{keyword "open"} >> K false) -- Scan.option Parse.binding ||
    3.11          Parse.binding >> (fn s => (true, SOME s)))
    3.12 -        --| Parse.$$$ ")") (true, NONE) --
    3.13 +        --| @{keyword ")"}) (true, NONE) --
    3.14      (Parse.type_args_constrained -- Parse.binding) -- Parse.opt_mixfix --
    3.15 -    (Parse.$$$ "=" |-- Parse.term) --
    3.16 -    Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding))
    3.17 +    (@{keyword "="} |-- Parse.term) --
    3.18 +    Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
    3.19  
    3.20  fun mk_pcpodef_proof pcpo ((((((def, opt_name), (args, t)), mx), A), morphs)) =
    3.21    (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)

     4.1 --- a/src/HOL/HOLCF/Tools/domaindef.ML	Thu Mar 15 19:48:19 2012 +0100
     4.2 +++ b/src/HOL/HOLCF/Tools/domaindef.ML	Thu Mar 15 20:07:00 2012 +0100
     4.3 @@ -212,13 +212,13 @@
     4.4  (** outer syntax **)
     4.5  
     4.6  val domaindef_decl =
     4.7 -  Scan.optional (Parse.$$$ "(" |--
     4.8 -      ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
     4.9 +  Scan.optional (@{keyword "("} |--
    4.10 +      ((@{keyword "open"} >> K false) -- Scan.option Parse.binding ||
    4.11          Parse.binding >> (fn s => (true, SOME s)))
    4.12 -        --| Parse.$$$ ")") (true, NONE) --
    4.13 +        --| @{keyword ")"}) (true, NONE) --
    4.14      (Parse.type_args_constrained -- Parse.binding) --
    4.15 -    Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.term) --
    4.16 -    Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding))
    4.17 +    Parse.opt_mixfix -- (@{keyword "="} |-- Parse.term) --
    4.18 +    Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
    4.19  
    4.20  fun mk_domaindef ((((((def, opt_name), (args, t)), mx), A), morphs)) =
    4.21    domaindef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs)

     5.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Thu Mar 15 19:48:19 2012 +0100
     5.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Thu Mar 15 20:07:00 2012 +0100
     5.3 @@ -391,15 +391,15 @@
     5.4  (*************************************************************************)
     5.5  
     5.6  val opt_thm_name' : (bool * Attrib.binding) parser =
     5.7 -  Parse.$$$ "(" -- Parse.$$$ "unchecked" -- Parse.$$$ ")" >> K (true, Attrib.empty_binding)
     5.8 +  @{keyword "("} -- @{keyword "unchecked"} -- @{keyword ")"} >> K (true, Attrib.empty_binding)
     5.9      || Parse_Spec.opt_thm_name ":" >> pair false
    5.10  
    5.11  val spec' : (bool * (Attrib.binding * string)) parser =
    5.12    opt_thm_name' -- Parse.prop >> (fn ((a, b), c) => (a, (b, c)))
    5.13  
    5.14  val alt_specs' : (bool * (Attrib.binding * string)) list parser =
    5.15 -  let val unexpected = Scan.ahead (Parse.name || Parse.$$$ "[" || Parse.$$$ "(")
    5.16 -  in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! (Parse.$$$ "|"))) end
    5.17 +  let val unexpected = Scan.ahead (Parse.name || @{keyword "["} || @{keyword "("})
    5.18 +  in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! (@{keyword "|"}))) end
    5.19  
    5.20  val _ =
    5.21    Outer_Syntax.local_theory "fixrec" "define recursive functions (HOLCF)" Keyword.thy_decl

     6.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Thu Mar 15 19:48:19 2012 +0100
     6.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Mar 15 20:07:00 2012 +0100
     6.3 @@ -673,14 +673,14 @@
     6.4    Outer_Syntax.local_theory_to_proof "nominal_inductive"
     6.5      "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes"
     6.6      Keyword.thy_goal
     6.7 -    (Parse.xname -- Scan.optional (Parse.$$$ "avoids" |-- Parse.and_list1 (Parse.name --
     6.8 -      (Parse.$$$ ":" |-- Scan.repeat1 Parse.name))) [] >> (fn (name, avoids) =>
     6.9 +    (Parse.xname -- Scan.optional (@{keyword "avoids"} |-- Parse.and_list1 (Parse.name --
    6.10 +      (@{keyword ":"} |-- Scan.repeat1 Parse.name))) [] >> (fn (name, avoids) =>
    6.11          prove_strong_ind name avoids));
    6.12  
    6.13  val _ =
    6.14    Outer_Syntax.local_theory "equivariance"
    6.15      "prove equivariance for inductive predicate involving nominal datatypes" Keyword.thy_decl
    6.16 -    (Parse.xname -- Scan.optional (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]") [] >>
    6.17 +    (Parse.xname -- Scan.optional (@{keyword "["} |-- Parse.list1 Parse.name --| @{keyword "]"}) [] >>
    6.18        (fn (name, atoms) => prove_eqvt name atoms));
    6.19  
    6.20  end

     7.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Thu Mar 15 19:48:19 2012 +0100
     7.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Thu Mar 15 20:07:00 2012 +0100
     7.3 @@ -488,9 +488,9 @@
     7.4      "prove strong induction theorem for inductive predicate involving nominal datatypes"
     7.5      Keyword.thy_goal
     7.6      (Parse.xname -- 
     7.7 -     Scan.option (Parse.$$$ "(" |-- Parse.!!! (Parse.name --| Parse.$$$ ")")) --
     7.8 -     (Scan.optional (Parse.$$$ "avoids" |-- Parse.enum1 "|" (Parse.name --
     7.9 -      (Parse.$$$ ":" |-- Parse.and_list1 Parse.term))) []) >> (fn ((name, rule_name), avoids) =>
    7.10 +     Scan.option (@{keyword "("} |-- Parse.!!! (Parse.name --| @{keyword ")"})) --
    7.11 +     (Scan.optional (@{keyword "avoids"} |-- Parse.enum1 "|" (Parse.name --
    7.12 +      (@{keyword ":"} |-- Parse.and_list1 Parse.term))) []) >> (fn ((name, rule_name), avoids) =>
    7.13          prove_strong_ind name rule_name avoids));
    7.14  
    7.15  end

     8.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Thu Mar 15 19:48:19 2012 +0100
     8.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Thu Mar 15 20:07:00 2012 +0100
     8.3 @@ -392,14 +392,14 @@
     8.4  val freshness_context = Parse.reserved "freshness_context";
     8.5  val invariant = Parse.reserved "invariant";
     8.6  
     8.7 -fun unless_flag scan = Scan.unless ((freshness_context || invariant) -- Parse.$$$ ":") scan;
     8.8 +fun unless_flag scan = Scan.unless ((freshness_context || invariant) -- @{keyword ":"}) scan;
     8.9  
    8.10 -val parser1 = (freshness_context -- Parse.$$$ ":") |-- unless_flag Parse.term >> SOME;
    8.11 -val parser2 = (invariant -- Parse.$$$ ":") |--
    8.12 +val parser1 = (freshness_context -- @{keyword ":"}) |-- unless_flag Parse.term >> SOME;
    8.13 +val parser2 = (invariant -- @{keyword ":"}) |--
    8.14      (Scan.repeat1 (unless_flag Parse.term) >> SOME) -- Scan.optional parser1 NONE ||
    8.15    (parser1 >> pair NONE);
    8.16  val options =
    8.17 -  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (parser2 --| Parse.$$$ ")")) (NONE, NONE);
    8.18 +  Scan.optional (@{keyword "("} |-- Parse.!!! (parser2 --| @{keyword ")"})) (NONE, NONE);
    8.19  
    8.20  val _ =
    8.21    Outer_Syntax.local_theory_to_proof "nominal_primrec"

     9.1 --- a/src/HOL/Statespace/state_space.ML	Thu Mar 15 19:48:19 2012 +0100
     9.2 +++ b/src/HOL/Statespace/state_space.ML	Thu Mar 15 20:07:00 2012 +0100
     9.3 @@ -676,15 +676,15 @@
     9.4  
     9.5  val type_insts =
     9.6    Parse.typ >> single ||
     9.7 -  Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.typ --| Parse.$$$ ")")
     9.8 +  @{keyword "("} |-- Parse.!!! (Parse.list1 Parse.typ --| @{keyword ")"})
     9.9  
    9.10 -val comp = Parse.name -- (Parse.$$$ "::" |-- Parse.!!! Parse.typ);
    9.11 +val comp = Parse.name -- (@{keyword "::"} |-- Parse.!!! Parse.typ);
    9.12  fun plus1_unless test scan =
    9.13 -  scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan));
    9.14 +  scan ::: Scan.repeat (@{keyword "+"} |-- Scan.unless test (Parse.!!! scan));
    9.15  
    9.16 -val mapsto = Parse.$$$ "=";
    9.17 +val mapsto = @{keyword "="};
    9.18  val rename = Parse.name -- (mapsto |-- Parse.name);
    9.19 -val renames = Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.list1 rename --| Parse.$$$ "]")) [];
    9.20 +val renames = Scan.optional (@{keyword "["} |-- Parse.!!! (Parse.list1 rename --| @{keyword "]"})) [];
    9.21  
    9.22  val parent =
    9.23    ((type_insts -- Parse.xname) || (Parse.xname >> pair [])) -- renames
    9.24 @@ -694,10 +694,10 @@
    9.25  
    9.26  val statespace_decl =
    9.27    Parse.type_args -- Parse.name --
    9.28 -    (Parse.$$$ "=" |--
    9.29 +    (@{keyword "="} |--
    9.30        ((Scan.repeat1 comp >> pair []) ||
    9.31          (plus1_unless comp parent --
    9.32 -          Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 comp)) [])));
    9.33 +          Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 comp)) [])));
    9.34  val _ =
    9.35    Outer_Syntax.command "statespace" "define state space" Keyword.thy_decl
    9.36      (statespace_decl >> (fn ((args, name), (parents, comps)) =>

    10.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Thu Mar 15 19:48:19 2012 +0100
    10.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Thu Mar 15 20:07:00 2012 +0100
    10.3 @@ -788,7 +788,7 @@
    10.4  
    10.5  val spec_cmd =
    10.6    Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
    10.7 -  (Parse.$$$ "=" |-- Parse.enum1 "|" (Parse.binding -- Scan.repeat Parse.typ -- Parse.opt_mixfix))
    10.8 +  (@{keyword "="} |-- Parse.enum1 "|" (Parse.binding -- Scan.repeat Parse.typ -- Parse.opt_mixfix))
    10.9    >> (fn (((vs, t), mx), cons) => ((t, vs, mx), map Parse.triple1 cons));
   10.10  
   10.11  val _ =

    11.1 --- a/src/HOL/Tools/Function/function_common.ML	Thu Mar 15 19:48:19 2012 +0100
    11.2 +++ b/src/HOL/Tools/Function/function_common.ML	Thu Mar 15 20:07:00 2012 +0100
    11.3 @@ -345,7 +345,7 @@
    11.4       || (Parse.reserved "no_partials" >> K No_Partials))
    11.5  
    11.6    fun config_parser default =
    11.7 -    (Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 option_parser) --| Parse.$$$ ")") [])
    11.8 +    (Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 option_parser) --| @{keyword ")"}) [])
    11.9       >> (fn opts => fold apply_opt opts default)
   11.10  in
   11.11    fun function_parser default_cfg =

    12.1 --- a/src/HOL/Tools/Function/partial_function.ML	Thu Mar 15 19:48:19 2012 +0100
    12.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Thu Mar 15 20:07:00 2012 +0100
    12.3 @@ -279,7 +279,7 @@
    12.4  val add_partial_function = gen_add_partial_function Specification.check_spec;
    12.5  val add_partial_function_cmd = gen_add_partial_function Specification.read_spec;
    12.6  
    12.7 -val mode = Parse.$$$ "(" |-- Parse.xname --| Parse.$$$ ")";
    12.8 +val mode = @{keyword "("} |-- Parse.xname --| @{keyword ")"};
    12.9  
   12.10  val _ = Outer_Syntax.local_theory
   12.11    "partial_function" "define partial function" Keyword.thy_decl

    13.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Thu Mar 15 19:48:19 2012 +0100
    13.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Thu Mar 15 20:07:00 2012 +0100
    13.3 @@ -292,7 +292,7 @@
    13.4  val parse_metis_options =
    13.5    Scan.optional
    13.6        (Args.parens (Parse.short_ident
    13.7 -                    -- Scan.option (Parse.$$$ "," |-- Parse.short_ident))
    13.8 +                    -- Scan.option (@{keyword ","} |-- Parse.short_ident))
    13.9         >> (fn (s, s') =>
   13.10                (NONE, NONE) |> consider_opt s
   13.11                             |> (case s' of SOME s' => consider_opt s' | _ => I)))

    14.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Thu Mar 15 19:48:19 2012 +0100
    14.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Thu Mar 15 20:07:00 2012 +0100
    14.3 @@ -317,11 +317,11 @@
    14.4    Scan.repeat1 (Parse.minus >> single
    14.5                  || Scan.repeat1 (Scan.unless Parse.minus
    14.6                                               (Parse.name || Parse.float_number))
    14.7 -                || Parse.$$$ "," |-- Parse.number >> prefix "," >> single)
    14.8 +                || @{keyword ","} |-- Parse.number >> prefix "," >> single)
    14.9    >> flat
   14.10 -val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
   14.11 +val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) []
   14.12  val parse_params =
   14.13 -  Scan.optional (Parse.$$$ "[" |-- Parse.list parse_param --| Parse.$$$ "]") []
   14.14 +  Scan.optional (@{keyword "["} |-- Parse.list parse_param --| @{keyword "]"}) []
   14.15  
   14.16  fun handle_exceptions ctxt f x =
   14.17    f x

    15.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Mar 15 19:48:19 2012 +0100
    15.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Mar 15 20:07:00 2012 +0100
    15.3 @@ -1002,7 +1002,7 @@
    15.4  (* renewing the values command for Prolog queries *)
    15.5  
    15.6  val opt_print_modes =
    15.7 -  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
    15.8 +  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
    15.9  
   15.10  val _ = Outer_Syntax.improper_command "values" "enumerate and print comprehensions" Keyword.diag
   15.11    (opt_print_modes -- Scan.optional (Parse.nat >> SOME) NONE -- Parse.term

    16.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Thu Mar 15 19:48:19 2012 +0100
    16.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Thu Mar 15 20:07:00 2012 +0100
    16.3 @@ -221,15 +221,15 @@
    16.4  
    16.5  
    16.6  val opt_modes =
    16.7 -  Scan.optional (Parse.$$$ "(" |-- Args.$$$ "modes" |-- Parse.$$$ ":" |--
    16.8 -    (((Parse.enum1 "and" (Parse.xname --| Parse.$$$ ":" --
    16.9 +  Scan.optional (@{keyword "("} |-- Args.$$$ "modes" |-- @{keyword ":"} |--
   16.10 +    (((Parse.enum1 "and" (Parse.xname --| @{keyword ":"} --
   16.11          (Parse.enum "," mode_and_opt_proposal))) >> Multiple_Preds)
   16.12        || ((Parse.enum "," mode_and_opt_proposal) >> Single_Pred))
   16.13 -    --| Parse.$$$ ")") (Multiple_Preds [])
   16.14 +    --| @{keyword ")"}) (Multiple_Preds [])
   16.15  
   16.16  val opt_expected_modes =
   16.17 -  Scan.optional (Parse.$$$ "(" |-- Args.$$$ "expected_modes" |-- Parse.$$$ ":" |--
   16.18 -    Parse.enum "," parse_mode_expr --| Parse.$$$ ")" >> SOME) NONE
   16.19 +  Scan.optional (@{keyword "("} |-- Args.$$$ "expected_modes" |-- @{keyword ":"} |--
   16.20 +    Parse.enum "," parse_mode_expr --| @{keyword ")"} >> SOME) NONE
   16.21  
   16.22  (* Parser for options *)
   16.23  
   16.24 @@ -238,18 +238,18 @@
   16.25      val scan_bool_option = foldl1 (op ||) (map Args.$$$ bool_options)
   16.26      val scan_compilation = foldl1 (op ||) (map (fn (s, c) => Args.$$$ s >> K c) compilation_names)
   16.27    in
   16.28 -    Scan.optional (Parse.$$$ "[" |-- Scan.optional scan_compilation Pred
   16.29 -      -- Parse.enum "," scan_bool_option --| Parse.$$$ "]")
   16.30 +    Scan.optional (@{keyword "["} |-- Scan.optional scan_compilation Pred
   16.31 +      -- Parse.enum "," scan_bool_option --| @{keyword "]"})
   16.32        (Pred, [])
   16.33    end
   16.34  
   16.35  val opt_print_modes =
   16.36 -  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
   16.37 +  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
   16.38  
   16.39 -val opt_mode = (Parse.$$$ "_" >> K NONE) || (parse_mode_expr >> SOME)
   16.40 +val opt_mode = (Args.$$$ "_" >> K NONE) || (parse_mode_expr >> SOME)
   16.41  
   16.42 -val opt_param_modes = Scan.optional (Parse.$$$ "[" |-- Args.$$$ "mode" |-- Parse.$$$ ":" |--
   16.43 -  Parse.enum ", " opt_mode --| Parse.$$$ "]" >> SOME) NONE
   16.44 +val opt_param_modes = Scan.optional (@{keyword "["} |-- Args.$$$ "mode" |-- @{keyword ":"} |--
   16.45 +  Parse.enum ", " opt_mode --| @{keyword "]"} >> SOME) NONE
   16.46  
   16.47  val stats = Scan.optional (Args.$$$ "stats" >> K true) false
   16.48  
   16.49 @@ -264,7 +264,7 @@
   16.50          (Pred, [])
   16.51    in
   16.52      Scan.optional
   16.53 -      (Parse.$$$ "[" |-- (expected_values -- stats) -- scan_compilation --| Parse.$$$ "]")
   16.54 +      (@{keyword "["} |-- (expected_values -- stats) -- scan_compilation --| @{keyword "]"})
   16.55        ((NONE, false), (Pred, []))
   16.56    end
   16.57  

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

    18.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Thu Mar 15 19:48:19 2012 +0100
    18.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Thu Mar 15 20:07:00 2012 +0100
    18.3 @@ -109,7 +109,7 @@
    18.4  (* parser and command *)
    18.5  val quotdef_parser =
    18.6    Scan.option Parse_Spec.constdecl --
    18.7 -    Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| Parse.$$$ "is" -- Parse.term))
    18.8 +    Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| @{keyword "is"} -- Parse.term))
    18.9  
   18.10  val _ =
   18.11    Outer_Syntax.local_theory "quotient_definition"

    19.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Thu Mar 15 19:48:19 2012 +0100
    19.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Thu Mar 15 20:07:00 2012 +0100
    19.3 @@ -71,7 +71,7 @@
    19.4  
    19.5  val quotmaps_attribute_setup =
    19.6    Attrib.setup @{binding map}
    19.7 -    ((Args.type_name false --| Scan.lift (Parse.$$$ "=")) --  (* FIXME Args.type_name true (requires "set" type) *)
    19.8 +    ((Args.type_name false --| Scan.lift (@{keyword "="})) --  (* FIXME Args.type_name true (requires "set" type) *)
    19.9        Args.const_proper true >>
   19.10        (fn (tyname, relname) =>
   19.11          let val minfo = {relmap = relname}

    20.1 --- a/src/HOL/Tools/Quotient/quotient_type.ML	Thu Mar 15 19:48:19 2012 +0100
    20.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML	Thu Mar 15 20:07:00 2012 +0100
    20.3 @@ -262,15 +262,15 @@
    20.4      quotient_type spec' lthy
    20.5    end
    20.6  
    20.7 -val partial = Scan.optional (Parse.reserved "partial" -- Parse.$$$ ":" >> K true) false
    20.8 +val partial = Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false
    20.9  
   20.10  val quotspec_parser =
   20.11    Parse.and_list1
   20.12      ((Parse.type_args -- Parse.binding) --
   20.13        (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *)
   20.14 -      Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) --
   20.15 -        (Parse.$$$ "/" |-- (partial -- Parse.term))  --
   20.16 -        Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding)))
   20.17 +      Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --
   20.18 +        (@{keyword "/"} |-- (partial -- Parse.term))  --
   20.19 +        Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)))
   20.20  
   20.21  val _ =
   20.22    Outer_Syntax.local_theory_to_proof "quotient_type"

    21.1 --- a/src/HOL/Tools/SMT/smt_config.ML	Thu Mar 15 19:48:19 2012 +0100
    21.2 +++ b/src/HOL/Tools/SMT/smt_config.ML	Thu Mar 15 20:07:00 2012 +0100
    21.3 @@ -86,7 +86,7 @@
    21.4      context
    21.5      |> Solvers.map (apfst (Symtab.update (name, (info, []))))
    21.6      |> Context.map_theory (Attrib.setup (Binding.name (name ^ "_options"))
    21.7 -        (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
    21.8 +        (Scan.lift (@{keyword "="} |-- Args.name) >>
    21.9            (Thm.declaration_attribute o K o set_solver_options o pair name))
   21.10          ("Additional command line options for SMT solver " ^ quote name))
   21.11  
   21.12 @@ -142,7 +142,7 @@
   21.13  
   21.14  val setup_solver =
   21.15    Attrib.setup @{binding smt_solver}
   21.16 -    (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
   21.17 +    (Scan.lift (@{keyword "="} |-- Args.name) >>
   21.18        (Thm.declaration_attribute o K o select_solver))
   21.19      "SMT solver configuration"
   21.20  
   21.21 @@ -207,7 +207,7 @@
   21.22  
   21.23  val setup_certificates =
   21.24    Attrib.setup @{binding smt_certificates}
   21.25 -    (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
   21.26 +    (Scan.lift (@{keyword "="} |-- Args.name) >>
   21.27        (Thm.declaration_attribute o K o select_certificates))
   21.28      "SMT certificates configuration"
   21.29  

    22.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Mar 15 19:48:19 2012 +0100
    22.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Mar 15 20:07:00 2012 +0100
    22.3 @@ -396,12 +396,12 @@
    22.4                                         |> sort_strings |> cat_lines))
    22.5                    end))
    22.6  
    22.7 -val parse_query_bang = Parse.$$$ "?" || Parse.$$$ "!" || Parse.$$$ "!!"
    22.8 +val parse_query_bang = @{keyword "?"} || @{keyword "!"} || @{keyword "!!"}
    22.9  val parse_key =
   22.10    Scan.repeat1 (Parse.typ_group || parse_query_bang) >> implode_param
   22.11  val parse_value =
   22.12    Scan.repeat1 (Parse.xname || Parse.float_number || parse_query_bang)
   22.13 -val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
   22.14 +val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) []
   22.15  val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
   22.16  val parse_fact_refs =
   22.17    Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse_Spec.xthm)

    23.1 --- a/src/HOL/Tools/choice_specification.ML	Thu Mar 15 19:48:19 2012 +0100
    23.2 +++ b/src/HOL/Tools/choice_specification.ML	Thu Mar 15 20:07:00 2012 +0100
    23.3 @@ -234,11 +234,11 @@
    23.4  
    23.5  (* outer syntax *)
    23.6  
    23.7 -val opt_name = Scan.optional (Parse.name --| Parse.$$$ ":") ""
    23.8 +val opt_name = Scan.optional (Parse.name --| @{keyword ":"}) ""
    23.9  val opt_overloaded = Parse.opt_keyword "overloaded"
   23.10  
   23.11  val specification_decl =
   23.12 -  Parse.$$$ "(" |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| Parse.$$$ ")" --
   23.13 +  @{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} --
   23.14            Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop)
   23.15  
   23.16  val _ =
   23.17 @@ -249,7 +249,7 @@
   23.18  
   23.19  val ax_specification_decl =
   23.20      Parse.name --
   23.21 -    (Parse.$$$ "(" |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| Parse.$$$ ")" --
   23.22 +    (@{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} --
   23.23             Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop))
   23.24  
   23.25  val _ =

    24.1 --- a/src/HOL/Tools/enriched_type.ML	Thu Mar 15 19:48:19 2012 +0100
    24.2 +++ b/src/HOL/Tools/enriched_type.ML	Thu Mar 15 20:07:00 2012 +0100
    24.3 @@ -268,7 +268,7 @@
    24.4  
    24.5  val _ = Outer_Syntax.local_theory_to_proof "enriched_type"
    24.6    "register operations managing the functorial structure of a type"
    24.7 -  Keyword.thy_goal (Scan.option (Parse.name --| Parse.$$$ ":") -- Parse.term
    24.8 +  Keyword.thy_goal (Scan.option (Parse.name --| @{keyword ":"}) -- Parse.term
    24.9      >> (fn (prfx, t) => enriched_type_cmd prfx t));
   24.10  
   24.11  end;

    25.1 --- a/src/HOL/Tools/inductive.ML	Thu Mar 15 19:48:19 2012 +0100
    25.2 +++ b/src/HOL/Tools/inductive.ML	Thu Mar 15 20:07:00 2012 +0100
    25.3 @@ -1137,7 +1137,7 @@
    25.4  fun gen_ind_decl mk_def coind =
    25.5    Parse.fixes -- Parse.for_fixes --
    25.6    Scan.optional Parse_Spec.where_alt_specs [] --
    25.7 -  Scan.optional (Parse.$$$ "monos" |-- Parse.!!! Parse_Spec.xthms1) []
    25.8 +  Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse_Spec.xthms1) []
    25.9    >> (fn (((preds, params), specs), monos) =>
   25.10        (snd oo gen_add_inductive mk_def true coind preds params specs monos));
   25.11  

    26.1 --- a/src/HOL/Tools/recdef.ML	Thu Mar 15 19:48:19 2012 +0100
    26.2 +++ b/src/HOL/Tools/recdef.ML	Thu Mar 15 20:07:00 2012 +0100
    26.3 @@ -291,12 +291,12 @@
    26.4  (* outer syntax *)
    26.5  
    26.6  val hints =
    26.7 -  Parse.$$$ "(" |--
    26.8 -    Parse.!!! (Parse.position (Parse.$$$ "hints" -- Args.parse) --| Parse.$$$ ")") >> Args.src;
    26.9 +  @{keyword "("} |--
   26.10 +    Parse.!!! (Parse.position (@{keyword "hints"} -- Args.parse) --| @{keyword ")"}) >> Args.src;
   26.11  
   26.12  val recdef_decl =
   26.13    Scan.optional
   26.14 -    (Parse.$$$ "(" -- Parse.!!! (Parse.$$$ "permissive" -- Parse.$$$ ")") >> K false) true --
   26.15 +    (@{keyword "("} -- Parse.!!! (@{keyword "permissive"} -- @{keyword ")"}) >> K false) true --
   26.16    Parse.name -- Parse.term -- Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)
   26.17      -- Scan.option hints
   26.18    >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map Parse.triple_swap eqs) src);
   26.19 @@ -309,7 +309,7 @@
   26.20  val defer_recdef_decl =
   26.21    Parse.name -- Scan.repeat1 Parse.prop --
   26.22    Scan.optional
   26.23 -    (Parse.$$$ "(" |-- Parse.$$$ "congs" |-- Parse.!!! (Parse_Spec.xthms1 --| Parse.$$$ ")")) []
   26.24 +    (@{keyword "("} |-- @{keyword "congs"} |-- Parse.!!! (Parse_Spec.xthms1 --| @{keyword ")"})) []
   26.25    >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
   26.26  
   26.27  val _ =
   26.28 @@ -320,7 +320,7 @@
   26.29    Outer_Syntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
   26.30      Keyword.thy_goal
   26.31      ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.xname --
   26.32 -        Scan.option (Parse.$$$ "(" |-- Parse.nat --| Parse.$$$ ")")
   26.33 +        Scan.option (@{keyword "("} |-- Parse.nat --| @{keyword ")"})
   26.34        >> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
   26.35  
   26.36  end;

    27.1 --- a/src/HOL/Tools/record.ML	Thu Mar 15 19:48:19 2012 +0100
    27.2 +++ b/src/HOL/Tools/record.ML	Thu Mar 15 20:07:00 2012 +0100
    27.3 @@ -2313,7 +2313,7 @@
    27.4  val _ =
    27.5    Outer_Syntax.command "record" "define extensible record" Keyword.thy_decl
    27.6      (Parse.type_args_constrained -- Parse.binding --
    27.7 -      (Parse.$$$ "=" |-- Scan.option (Parse.typ --| Parse.$$$ "+") --
    27.8 +      (@{keyword "="} |-- Scan.option (Parse.typ --| @{keyword "+"}) --
    27.9          Scan.repeat1 Parse.const_binding)
   27.10      >> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd x y z)));
   27.11  

    28.1 --- a/src/HOL/Tools/refute.ML	Thu Mar 15 19:48:19 2012 +0100
    28.2 +++ b/src/HOL/Tools/refute.ML	Thu Mar 15 20:07:00 2012 +0100
    28.3 @@ -3202,8 +3202,8 @@
    28.4  
    28.5  (*optional list of arguments of the form [name1=value1, name2=value2, ...]*)
    28.6  
    28.7 -val scan_parm = Parse.name -- (Scan.optional (Parse.$$$ "=" |-- Parse.name) "true")
    28.8 -val scan_parms = Scan.optional (Parse.$$$ "[" |-- Parse.list scan_parm --| Parse.$$$ "]") [];
    28.9 +val scan_parm = Parse.name -- (Scan.optional (@{keyword "="} |-- Parse.name) "true")
   28.10 +val scan_parms = Scan.optional (@{keyword "["} |-- Parse.list scan_parm --| @{keyword "]"}) [];
   28.11  
   28.12  
   28.13  (* 'refute' command *)

    29.1 --- a/src/HOL/Tools/typedef.ML	Thu Mar 15 19:48:19 2012 +0100
    29.2 +++ b/src/HOL/Tools/typedef.ML	Thu Mar 15 20:07:00 2012 +0100
    29.3 @@ -302,12 +302,12 @@
    29.4  val _ =
    29.5    Outer_Syntax.local_theory_to_proof "typedef" "HOL type definition (requires non-emptiness proof)"
    29.6      Keyword.thy_goal
    29.7 -    (Scan.optional (Parse.$$$ "(" |--
    29.8 -        ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
    29.9 -          Parse.binding >> (fn s => (true, SOME s))) --| Parse.$$$ ")") (true, NONE) --
   29.10 +    (Scan.optional (@{keyword "("} |--
   29.11 +        ((@{keyword "open"} >> K false) -- Scan.option Parse.binding ||
   29.12 +          Parse.binding >> (fn s => (true, SOME s))) --| @{keyword ")"}) (true, NONE) --
   29.13        (Parse.type_args_constrained -- Parse.binding) --
   29.14 -        Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.term) --
   29.15 -        Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding))
   29.16 +        Parse.opt_mixfix -- (@{keyword "="} |-- Parse.term) --
   29.17 +        Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
   29.18      >> (fn ((((((def, opt_name), (args, t)), mx), A), morphs)) =>
   29.19          typedef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs)));
   29.20  

    30.1 --- a/src/Tools/Code/code_printer.ML	Thu Mar 15 19:48:19 2012 +0100
    30.2 +++ b/src/Tools/Code/code_printer.ML	Thu Mar 15 20:07:00 2012 +0100
    30.3 @@ -394,13 +394,11 @@
    30.4      | _ => Scan.!! (err s) Scan.fail ()
    30.5    end;
    30.6  
    30.7 -val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr");
    30.8 -
    30.9  fun parse_syntax mk_plain mk_complex prep_arg =
   30.10    Scan.option (
   30.11 -      ((Parse.$$$ infixK >> K X)
   30.12 -        || (Parse.$$$ infixlK >> K L)
   30.13 -        || (Parse.$$$ infixrK >> K R))
   30.14 +      ((@{keyword "infix"} >> K X)
   30.15 +        || (@{keyword "infixl"} >> K L)
   30.16 +        || (@{keyword "infixr"} >> K R))
   30.17          -- Parse.nat -- Parse.string
   30.18          >> (fn ((x, i), s) => mk_complex (parse_infix prep_arg (x, i) s))
   30.19        || Parse.string >> (fn s => (parse_mixfix mk_plain mk_complex prep_arg s)));

    31.1 --- a/src/Tools/Code/code_runtime.ML	Thu Mar 15 19:48:19 2012 +0100
    31.2 +++ b/src/Tools/Code/code_runtime.ML	Thu Mar 15 20:07:00 2012 +0100
    31.3 @@ -344,24 +344,19 @@
    31.4  
    31.5  local
    31.6  
    31.7 -val datatypesK = "datatypes";
    31.8 -val functionsK = "functions";
    31.9 -val fileK = "file";
   31.10 -val andK = "and"
   31.11 -
   31.12  val parse_datatype =
   31.13 -  Parse.name --| Parse.$$$ "=" --
   31.14 +  Parse.name --| @{keyword "="} --
   31.15      (((Parse.sym_ident || Parse.string) >> (fn "_" => NONE | _ => Scan.fail ()))
   31.16 -    || ((Parse.term ::: (Scan.repeat (Parse.$$$ "|" |-- Parse.term))) >> SOME));
   31.17 +    || ((Parse.term ::: (Scan.repeat (@{keyword "|"} |-- Parse.term))) >> SOME));
   31.18  
   31.19  in
   31.20  
   31.21  val _ =
   31.22    Outer_Syntax.command "code_reflect" "enrich runtime environment with generated code"
   31.23 -    Keyword.thy_decl (Parse.name -- Scan.optional (Parse.$$$ datatypesK |-- (parse_datatype
   31.24 -      ::: Scan.repeat (Parse.$$$ andK |-- parse_datatype))) []
   31.25 -    -- Scan.optional (Parse.$$$ functionsK |-- Scan.repeat1 Parse.name) []
   31.26 -    -- Scan.option (Parse.$$$ fileK |-- Parse.name)
   31.27 +    Keyword.thy_decl (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- (parse_datatype
   31.28 +      ::: Scan.repeat (@{keyword "and"} |-- parse_datatype))) []
   31.29 +    -- Scan.optional (@{keyword "functions"} |-- Scan.repeat1 Parse.name) []
   31.30 +    -- Scan.option (@{keyword "file"} |-- Parse.name)
   31.31    >> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory
   31.32      (code_reflect_cmd raw_datatypes raw_functions module_name some_file)));
   31.33  

    32.1 --- a/src/Tools/Code/code_target.ML	Thu Mar 15 19:48:19 2012 +0100
    32.2 +++ b/src/Tools/Code/code_target.ML	Thu Mar 15 20:07:00 2012 +0100
    32.3 @@ -638,8 +638,8 @@
    32.4  
    32.5  fun process_multi_syntax parse_thing parse_syntax change =
    32.6    (Parse.and_list1 parse_thing
    32.7 -  :|-- (fn things => Scan.repeat1 (Parse.$$$ "(" |-- Parse.name --
    32.8 -        (zip_list things parse_syntax (Parse.$$$ "and")) --| Parse.$$$ ")")))
    32.9 +  :|-- (fn things => Scan.repeat1 (@{keyword "("} |-- Parse.name --
   32.10 +        (zip_list things parse_syntax (@{keyword "and"})) --| @{keyword ")"})))
   32.11    >> (Toplevel.theory oo fold)
   32.12      (fn (target, syns) => fold (fn (raw_x, syn) => change target raw_x syn) syns);
   32.13  
   32.14 @@ -667,18 +667,16 @@
   32.15  
   32.16  (** Isar setup **)
   32.17  
   32.18 -val (inK, module_nameK, fileK, checkingK) = ("in", "module_name", "file", "checking");
   32.19 -
   32.20 -val code_expr_argsP = Scan.optional (Parse.$$$ "(" |-- Args.parse --| Parse.$$$ ")") [];
   32.21 +val code_expr_argsP = Scan.optional (@{keyword "("} |-- Args.parse --| @{keyword ")"}) [];
   32.22  
   32.23  val code_exprP =
   32.24    Scan.repeat1 Parse.term_group :|-- (fn raw_cs =>
   32.25 -    ((Parse.$$$ checkingK |-- Scan.repeat (Parse.name
   32.26 -      -- ((Parse.$$$ "?" |-- Scan.succeed false) || Scan.succeed true) -- code_expr_argsP))
   32.27 +    ((@{keyword "checking"} |-- Scan.repeat (Parse.name
   32.28 +      -- ((@{keyword "?"} |-- Scan.succeed false) || Scan.succeed true) -- code_expr_argsP))
   32.29        >> (fn seris => check_code_cmd raw_cs seris)
   32.30 -    || Scan.repeat (Parse.$$$ inK |-- Parse.name
   32.31 -       -- Scan.optional (Parse.$$$ module_nameK |-- Parse.name) ""
   32.32 -       -- Scan.optional (Parse.$$$ fileK |-- Parse.name) ""
   32.33 +    || Scan.repeat (@{keyword "in"} |-- Parse.name
   32.34 +       -- Scan.optional (@{keyword "module_name"} |-- Parse.name) ""
   32.35 +       -- Scan.optional (@{keyword "file"} |-- Parse.name) ""
   32.36         -- code_expr_argsP) >> (fn seris => export_code_cmd raw_cs seris)));
   32.37  
   32.38  val _ =
   32.39 @@ -688,7 +686,7 @@
   32.40  
   32.41  val _ =
   32.42    Outer_Syntax.command "code_instance" "define code syntax for instance" Keyword.thy_decl (
   32.43 -    process_multi_syntax (Parse.xname --| Parse.$$$ "::" -- Parse.xname)
   32.44 +    process_multi_syntax (Parse.xname --| @{keyword "::"} -- Parse.xname)
   32.45        (Scan.option (Parse.minus >> K ()))
   32.46      add_instance_syntax_cmd);
   32.47  
   32.48 @@ -713,7 +711,7 @@
   32.49    Outer_Syntax.command "code_include" "declare piece of code to be included in generated code"
   32.50      Keyword.thy_decl (
   32.51      Parse.name -- Parse.name -- (Parse.text :|-- (fn "-" => Scan.succeed NONE
   32.52 -      | s => Scan.optional (Parse.$$$ "attach" |-- Scan.repeat1 Parse.term) [] >> pair s >> SOME))
   32.53 +      | s => Scan.optional (@{keyword "attach"} |-- Scan.repeat1 Parse.term) [] >> pair s >> SOME))
   32.54      >> (fn ((target, name), content_consts) =>
   32.55          (Toplevel.theory o add_include_cmd target) (name, content_consts))
   32.56    );

    33.1 --- a/src/Tools/interpretation_with_defs.ML	Thu Mar 15 19:48:19 2012 +0100
    33.2 +++ b/src/Tools/interpretation_with_defs.ML	Thu Mar 15 20:07:00 2012 +0100
    33.3 @@ -83,8 +83,8 @@
    33.4    Outer_Syntax.command "interpretation"
    33.5      "prove interpretation of locale expression in theory" Keyword.thy_goal
    33.6      (Parse.!!! (Parse_Spec.locale_expression true) --
    33.7 -      Scan.optional (Parse.$$$ "defines" |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
    33.8 -        -- ((Parse.binding -- Parse.opt_mixfix') --| Parse.$$$ "is" -- Parse.term))) [] --
    33.9 +      Scan.optional (@{keyword "defines"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
   33.10 +        -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "is"} -- Parse.term))) [] --
   33.11        Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
   33.12        >> (fn ((expr, defs), equations) => Toplevel.print o
   33.13            Toplevel.theory_to_proof (interpretation_cmd expr defs equations)));

    34.1 --- a/src/Tools/quickcheck.ML	Thu Mar 15 19:48:19 2012 +0100
    34.2 +++ b/src/Tools/quickcheck.ML	Thu Mar 15 20:07:00 2012 +0100
    34.3 @@ -522,12 +522,12 @@
    34.4  
    34.5  val parse_arg =
    34.6    Parse.name --
    34.7 -    (Scan.optional (Parse.$$$ "=" |--
    34.8 +    (Scan.optional (@{keyword "="} |--
    34.9        (((Parse.name || Parse.float_number) >> single) ||
   34.10 -        (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]"))) ["true"]);
   34.11 +        (@{keyword "["} |-- Parse.list1 Parse.name --| @{keyword "]"}))) ["true"]);
   34.12  
   34.13  val parse_args =
   34.14 -  Parse.$$$ "[" |-- Parse.list1 parse_arg --| Parse.$$$ "]" || Scan.succeed [];
   34.15 +  @{keyword "["} |-- Parse.list1 parse_arg --| @{keyword "]"} || Scan.succeed [];
   34.16  
   34.17  val _ =
   34.18    Outer_Syntax.command quickcheck_paramsN "set parameters for random testing" Keyword.thy_decl

    35.1 --- a/src/Tools/value.ML	Thu Mar 15 19:48:19 2012 +0100
    35.2 +++ b/src/Tools/value.ML	Thu Mar 15 20:07:00 2012 +0100
    35.3 @@ -57,10 +57,10 @@
    35.4    in Pretty.writeln p end;
    35.5  
    35.6  val opt_modes =
    35.7 -  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
    35.8 +  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
    35.9  
   35.10  val opt_evaluator =
   35.11 -  Scan.option (Parse.$$$ "[" |-- Parse.xname --| Parse.$$$ "]")
   35.12 +  Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"})
   35.13    
   35.14  val _ =
   35.15    Outer_Syntax.improper_command "value" "evaluate and print term" Keyword.diag

    36.1 --- a/src/ZF/Tools/datatype_package.ML	Thu Mar 15 19:48:19 2012 +0100
    36.2 +++ b/src/ZF/Tools/datatype_package.ML	Thu Mar 15 20:07:00 2012 +0100
    36.3 @@ -427,15 +427,15 @@
    36.4    #1 o add_datatype (dom, map fst dts) (map snd dts) (monos, type_intrs, type_elims);
    36.5  
    36.6  val con_decl =
    36.7 -  Parse.name -- Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.term --| Parse.$$$ ")") [] --
    36.8 +  Parse.name -- Scan.optional (@{keyword "("} |-- Parse.list1 Parse.term --| @{keyword ")"}) [] --
    36.9      Parse.opt_mixfix >> Parse.triple1;
   36.10  
   36.11  val datatype_decl =
   36.12 -  (Scan.optional ((Parse.$$$ "\<subseteq>" || Parse.$$$ "<=") |-- Parse.!!! Parse.term) "") --
   36.13 -  Parse.and_list1 (Parse.term -- (Parse.$$$ "=" |-- Parse.enum1 "|" con_decl)) --
   36.14 -  Scan.optional (Parse.$$$ "monos" |-- Parse.!!! Parse_Spec.xthms1) [] --
   36.15 -  Scan.optional (Parse.$$$ "type_intros" |-- Parse.!!! Parse_Spec.xthms1) [] --
   36.16 -  Scan.optional (Parse.$$$ "type_elims" |-- Parse.!!! Parse_Spec.xthms1) []
   36.17 +  (Scan.optional ((@{keyword "\<subseteq>"} || @{keyword "<="}) |-- Parse.!!! Parse.term) "") --
   36.18 +  Parse.and_list1 (Parse.term -- (@{keyword "="} |-- Parse.enum1 "|" con_decl)) --
   36.19 +  Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse_Spec.xthms1) [] --
   36.20 +  Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse_Spec.xthms1) [] --
   36.21 +  Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse_Spec.xthms1) []
   36.22    >> (Toplevel.theory o mk_datatype);
   36.23  
   36.24  val coind_prefix = if coind then "co" else "";

    37.1 --- a/src/ZF/Tools/induct_tacs.ML	Thu Mar 15 19:48:19 2012 +0100
    37.2 +++ b/src/ZF/Tools/induct_tacs.ML	Thu Mar 15 20:07:00 2012 +0100
    37.3 @@ -189,10 +189,10 @@
    37.4  (* outer syntax *)
    37.5  
    37.6  val rep_datatype_decl =
    37.7 -  (Parse.$$$ "elimination" |-- Parse.!!! Parse_Spec.xthm) --
    37.8 -  (Parse.$$$ "induction" |-- Parse.!!! Parse_Spec.xthm) --
    37.9 -  (Parse.$$$ "case_eqns" |-- Parse.!!! Parse_Spec.xthms1) --
   37.10 -  Scan.optional (Parse.$$$ "recursor_eqns" |-- Parse.!!! Parse_Spec.xthms1) []
   37.11 +  (@{keyword "elimination"} |-- Parse.!!! Parse_Spec.xthm) --
   37.12 +  (@{keyword "induction"} |-- Parse.!!! Parse_Spec.xthm) --
   37.13 +  (@{keyword "case_eqns"} |-- Parse.!!! Parse_Spec.xthms1) --
   37.14 +  Scan.optional (@{keyword "recursor_eqns"} |-- Parse.!!! Parse_Spec.xthms1) []
   37.15    >> (fn (((x, y), z), w) => rep_datatype x y z w);
   37.16  
   37.17  val _ =

    38.1 --- a/src/ZF/Tools/inductive_package.ML	Thu Mar 15 19:48:19 2012 +0100
    38.2 +++ b/src/ZF/Tools/inductive_package.ML	Thu Mar 15 20:07:00 2012 +0100
    38.3 @@ -580,14 +580,14 @@
    38.4    #1 o add_inductive doms (map Parse.triple_swap intrs) (monos, con_defs, type_intrs, type_elims);
    38.5  
    38.6  val ind_decl =
    38.7 -  (Parse.$$$ "domains" |-- Parse.!!! (Parse.enum1 "+" Parse.term --
    38.8 -      ((Parse.$$$ "\<subseteq>" || Parse.$$$ "<=") |-- Parse.term))) --
    38.9 -  (Parse.$$$ "intros" |--
   38.10 +  (@{keyword "domains"} |-- Parse.!!! (Parse.enum1 "+" Parse.term --
   38.11 +      ((@{keyword "\<subseteq>"} || @{keyword "<="}) |-- Parse.term))) --
   38.12 +  (@{keyword "intros"} |--
   38.13      Parse.!!! (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop))) --
   38.14 -  Scan.optional (Parse.$$$ "monos" |-- Parse.!!! Parse_Spec.xthms1) [] --
   38.15 -  Scan.optional (Parse.$$$ "con_defs" |-- Parse.!!! Parse_Spec.xthms1) [] --
   38.16 -  Scan.optional (Parse.$$$ "type_intros" |-- Parse.!!! Parse_Spec.xthms1) [] --
   38.17 -  Scan.optional (Parse.$$$ "type_elims" |-- Parse.!!! Parse_Spec.xthms1) []
   38.18 +  Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse_Spec.xthms1) [] --
   38.19 +  Scan.optional (@{keyword "con_defs"} |-- Parse.!!! Parse_Spec.xthms1) [] --
   38.20 +  Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse_Spec.xthms1) [] --
   38.21 +  Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse_Spec.xthms1) []
   38.22    >> (Toplevel.theory o mk_ind);
   38.23  
   38.24  val _ =