# HG changeset patch
# User wenzelm
# Date 1331838420 -3600
# Node ID 94aa7b81bcf69a77b653e623a2bb798c4d386b32
# Parent  aae5566d67562c1e40132bb381482a9eb0e525ef
prefer formally checked @{keyword} parser;

diff -r aae5566d6756 -r 94aa7b81bcf6 src/HOL/HOLCF/Tools/Domain/domain.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -229,21 +229,21 @@
 (** outer syntax **)
 
 val dest_decl : (bool * binding option * string) parser =
-  Parse.$$$ "(" |-- Scan.optional (Parse.$$$ "lazy" >> K true) false --
-    (Parse.binding >> SOME) -- (Parse.$$$ "::" |-- Parse.typ)  --| Parse.$$$ ")" >> Parse.triple1
-    || Parse.$$$ "(" |-- Parse.$$$ "lazy" |-- Parse.typ --| Parse.$$$ ")"
-    >> (fn t => (true,NONE,t))
-    || Parse.typ >> (fn t => (false,NONE,t))
+  @{keyword "("} |-- Scan.optional (@{keyword "lazy"} >> K true) false --
+    (Parse.binding >> SOME) -- (@{keyword "::"} |-- Parse.typ)  --| @{keyword ")"} >> Parse.triple1
+    || @{keyword "("} |-- @{keyword "lazy"} |-- Parse.typ --| @{keyword ")"}
+    >> (fn t => (true, NONE, t))
+    || Parse.typ >> (fn t => (false, NONE, t))
 
 val cons_decl =
   Parse.binding -- Scan.repeat dest_decl -- Parse.opt_mixfix
 
 val domain_decl =
   (Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix) --
-    (Parse.$$$ "=" |-- Parse.enum1 "|" cons_decl)
+    (@{keyword "="} |-- Parse.enum1 "|" cons_decl)
 
 val domains_decl =
-  Scan.optional (Parse.$$$ "(" |-- (Parse.$$$ "unsafe" >> K true) --| Parse.$$$ ")") false --
+  Scan.optional (@{keyword "("} |-- (@{keyword "unsafe"} >> K true) --| @{keyword ")"}) false --
     Parse.and_list1 domain_decl
 
 fun mk_domain
diff -r aae5566d6756 -r 94aa7b81bcf6 src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -762,8 +762,8 @@
 val parse_domain_iso :
     (string list * binding * mixfix * string * (binding * binding) option)
       parser =
-  (Parse.type_args -- Parse.binding -- Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) --
-    Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding)))
+  (Parse.type_args -- Parse.binding -- Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --
+    Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)))
     >> (fn ((((vs, t), mx), rhs), morphs) => (vs, t, mx, rhs, morphs))
 
 val parse_domain_isos = Parse.and_list1 parse_domain_iso
diff -r aae5566d6756 -r 94aa7b81bcf6 src/HOL/HOLCF/Tools/cpodef.ML
--- a/src/HOL/HOLCF/Tools/cpodef.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/HOLCF/Tools/cpodef.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -344,13 +344,13 @@
 (** outer syntax **)
 
 val typedef_proof_decl =
-  Scan.optional (Parse.$$$ "(" |--
-      ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
+  Scan.optional (@{keyword "("} |--
+      ((@{keyword "open"} >> K false) -- Scan.option Parse.binding ||
         Parse.binding >> (fn s => (true, SOME s)))
-        --| Parse.$$$ ")") (true, NONE) --
+        --| @{keyword ")"}) (true, NONE) --
     (Parse.type_args_constrained -- Parse.binding) -- Parse.opt_mixfix --
-    (Parse.$$$ "=" |-- Parse.term) --
-    Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding))
+    (@{keyword "="} |-- Parse.term) --
+    Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
 
 fun mk_pcpodef_proof pcpo ((((((def, opt_name), (args, t)), mx), A), morphs)) =
   (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
diff -r aae5566d6756 -r 94aa7b81bcf6 src/HOL/HOLCF/Tools/domaindef.ML
--- a/src/HOL/HOLCF/Tools/domaindef.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/HOLCF/Tools/domaindef.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -212,13 +212,13 @@
 (** outer syntax **)
 
 val domaindef_decl =
-  Scan.optional (Parse.$$$ "(" |--
-      ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
+  Scan.optional (@{keyword "("} |--
+      ((@{keyword "open"} >> K false) -- Scan.option Parse.binding ||
         Parse.binding >> (fn s => (true, SOME s)))
-        --| Parse.$$$ ")") (true, NONE) --
+        --| @{keyword ")"}) (true, NONE) --
     (Parse.type_args_constrained -- Parse.binding) --
-    Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.term) --
-    Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding))
+    Parse.opt_mixfix -- (@{keyword "="} |-- Parse.term) --
+    Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
 
 fun mk_domaindef ((((((def, opt_name), (args, t)), mx), A), morphs)) =
   domaindef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs)
diff -r aae5566d6756 -r 94aa7b81bcf6 src/HOL/HOLCF/Tools/fixrec.ML
--- a/src/HOL/HOLCF/Tools/fixrec.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/HOLCF/Tools/fixrec.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -391,15 +391,15 @@
 (*************************************************************************)
 
 val opt_thm_name' : (bool * Attrib.binding) parser =
-  Parse.$$$ "(" -- Parse.$$$ "unchecked" -- Parse.$$$ ")" >> K (true, Attrib.empty_binding)
+  @{keyword "("} -- @{keyword "unchecked"} -- @{keyword ")"} >> K (true, Attrib.empty_binding)
     || Parse_Spec.opt_thm_name ":" >> pair false
 
 val spec' : (bool * (Attrib.binding * string)) parser =
   opt_thm_name' -- Parse.prop >> (fn ((a, b), c) => (a, (b, c)))
 
 val alt_specs' : (bool * (Attrib.binding * string)) list parser =
-  let val unexpected = Scan.ahead (Parse.name || Parse.$$$ "[" || Parse.$$$ "(")
-  in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! (Parse.$$$ "|"))) end
+  let val unexpected = Scan.ahead (Parse.name || @{keyword "["} || @{keyword "("})
+  in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! (@{keyword "|"}))) end
 
 val _ =
   Outer_Syntax.local_theory "fixrec" "define recursive functions (HOLCF)" Keyword.thy_decl
diff -r aae5566d6756 -r 94aa7b81bcf6 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -673,14 +673,14 @@
   Outer_Syntax.local_theory_to_proof "nominal_inductive"
     "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes"
     Keyword.thy_goal
-    (Parse.xname -- Scan.optional (Parse.$$$ "avoids" |-- Parse.and_list1 (Parse.name --
-      (Parse.$$$ ":" |-- Scan.repeat1 Parse.name))) [] >> (fn (name, avoids) =>
+    (Parse.xname -- Scan.optional (@{keyword "avoids"} |-- Parse.and_list1 (Parse.name --
+      (@{keyword ":"} |-- Scan.repeat1 Parse.name))) [] >> (fn (name, avoids) =>
         prove_strong_ind name avoids));
 
 val _ =
   Outer_Syntax.local_theory "equivariance"
     "prove equivariance for inductive predicate involving nominal datatypes" Keyword.thy_decl
-    (Parse.xname -- Scan.optional (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]") [] >>
+    (Parse.xname -- Scan.optional (@{keyword "["} |-- Parse.list1 Parse.name --| @{keyword "]"}) [] >>
       (fn (name, atoms) => prove_eqvt name atoms));
 
 end
diff -r aae5566d6756 -r 94aa7b81bcf6 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -488,9 +488,9 @@
     "prove strong induction theorem for inductive predicate involving nominal datatypes"
     Keyword.thy_goal
     (Parse.xname -- 
-     Scan.option (Parse.$$$ "(" |-- Parse.!!! (Parse.name --| Parse.$$$ ")")) --
-     (Scan.optional (Parse.$$$ "avoids" |-- Parse.enum1 "|" (Parse.name --
-      (Parse.$$$ ":" |-- Parse.and_list1 Parse.term))) []) >> (fn ((name, rule_name), avoids) =>
+     Scan.option (@{keyword "("} |-- Parse.!!! (Parse.name --| @{keyword ")"})) --
+     (Scan.optional (@{keyword "avoids"} |-- Parse.enum1 "|" (Parse.name --
+      (@{keyword ":"} |-- Parse.and_list1 Parse.term))) []) >> (fn ((name, rule_name), avoids) =>
         prove_strong_ind name rule_name avoids));
 
 end
diff -r aae5566d6756 -r 94aa7b81bcf6 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -392,14 +392,14 @@
 val freshness_context = Parse.reserved "freshness_context";
 val invariant = Parse.reserved "invariant";
 
-fun unless_flag scan = Scan.unless ((freshness_context || invariant) -- Parse.$$$ ":") scan;
+fun unless_flag scan = Scan.unless ((freshness_context || invariant) -- @{keyword ":"}) scan;
 
-val parser1 = (freshness_context -- Parse.$$$ ":") |-- unless_flag Parse.term >> SOME;
-val parser2 = (invariant -- Parse.$$$ ":") |--
+val parser1 = (freshness_context -- @{keyword ":"}) |-- unless_flag Parse.term >> SOME;
+val parser2 = (invariant -- @{keyword ":"}) |--
     (Scan.repeat1 (unless_flag Parse.term) >> SOME) -- Scan.optional parser1 NONE ||
   (parser1 >> pair NONE);
 val options =
-  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (parser2 --| Parse.$$$ ")")) (NONE, NONE);
+  Scan.optional (@{keyword "("} |-- Parse.!!! (parser2 --| @{keyword ")"})) (NONE, NONE);
 
 val _ =
   Outer_Syntax.local_theory_to_proof "nominal_primrec"
diff -r aae5566d6756 -r 94aa7b81bcf6 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Statespace/state_space.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -676,15 +676,15 @@
 
 val type_insts =
   Parse.typ >> single ||
-  Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.typ --| Parse.$$$ ")")
+  @{keyword "("} |-- Parse.!!! (Parse.list1 Parse.typ --| @{keyword ")"})
 
-val comp = Parse.name -- (Parse.$$$ "::" |-- Parse.!!! Parse.typ);
+val comp = Parse.name -- (@{keyword "::"} |-- Parse.!!! Parse.typ);
 fun plus1_unless test scan =
-  scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan));
+  scan ::: Scan.repeat (@{keyword "+"} |-- Scan.unless test (Parse.!!! scan));
 
-val mapsto = Parse.$$$ "=";
+val mapsto = @{keyword "="};
 val rename = Parse.name -- (mapsto |-- Parse.name);
-val renames = Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.list1 rename --| Parse.$$$ "]")) [];
+val renames = Scan.optional (@{keyword "["} |-- Parse.!!! (Parse.list1 rename --| @{keyword "]"})) [];
 
 val parent =
   ((type_insts -- Parse.xname) || (Parse.xname >> pair [])) -- renames
@@ -694,10 +694,10 @@
 
 val statespace_decl =
   Parse.type_args -- Parse.name --
-    (Parse.$$$ "=" |--
+    (@{keyword "="} |--
       ((Scan.repeat1 comp >> pair []) ||
         (plus1_unless comp parent --
-          Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 comp)) [])));
+          Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 comp)) [])));
 val _ =
   Outer_Syntax.command "statespace" "define state space" Keyword.thy_decl
     (statespace_decl >> (fn ((args, name), (parents, comps)) =>
diff -r aae5566d6756 -r 94aa7b81bcf6 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -788,7 +788,7 @@
 
 val spec_cmd =
   Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
-  (Parse.$$$ "=" |-- Parse.enum1 "|" (Parse.binding -- Scan.repeat Parse.typ -- Parse.opt_mixfix))
+  (@{keyword "="} |-- Parse.enum1 "|" (Parse.binding -- Scan.repeat Parse.typ -- Parse.opt_mixfix))
   >> (fn (((vs, t), mx), cons) => ((t, vs, mx), map Parse.triple1 cons));
 
 val _ =
diff -r aae5566d6756 -r 94aa7b81bcf6 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/Function/function_common.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -345,7 +345,7 @@
      || (Parse.reserved "no_partials" >> K No_Partials))
 
   fun config_parser default =
-    (Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 option_parser) --| Parse.$$$ ")") [])
+    (Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 option_parser) --| @{keyword ")"}) [])
      >> (fn opts => fold apply_opt opts default)
 in
   fun function_parser default_cfg =
diff -r aae5566d6756 -r 94aa7b81bcf6 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -279,7 +279,7 @@
 val add_partial_function = gen_add_partial_function Specification.check_spec;
 val add_partial_function_cmd = gen_add_partial_function Specification.read_spec;
 
-val mode = Parse.$$$ "(" |-- Parse.xname --| Parse.$$$ ")";
+val mode = @{keyword "("} |-- Parse.xname --| @{keyword ")"};
 
 val _ = Outer_Syntax.local_theory
   "partial_function" "define partial function" Keyword.thy_decl
diff -r aae5566d6756 -r 94aa7b81bcf6 src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -292,7 +292,7 @@
 val parse_metis_options =
   Scan.optional
       (Args.parens (Parse.short_ident
-                    -- Scan.option (Parse.$$$ "," |-- Parse.short_ident))
+                    -- Scan.option (@{keyword ","} |-- Parse.short_ident))
        >> (fn (s, s') =>
               (NONE, NONE) |> consider_opt s
                            |> (case s' of SOME s' => consider_opt s' | _ => I)))
diff -r aae5566d6756 -r 94aa7b81bcf6 src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -317,11 +317,11 @@
   Scan.repeat1 (Parse.minus >> single
                 || Scan.repeat1 (Scan.unless Parse.minus
                                              (Parse.name || Parse.float_number))
-                || Parse.$$$ "," |-- Parse.number >> prefix "," >> single)
+                || @{keyword ","} |-- Parse.number >> prefix "," >> single)
   >> flat
-val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
+val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) []
 val parse_params =
-  Scan.optional (Parse.$$$ "[" |-- Parse.list parse_param --| Parse.$$$ "]") []
+  Scan.optional (@{keyword "["} |-- Parse.list parse_param --| @{keyword "]"}) []
 
 fun handle_exceptions ctxt f x =
   f x
diff -r aae5566d6756 -r 94aa7b81bcf6 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -1002,7 +1002,7 @@
 (* renewing the values command for Prolog queries *)
 
 val opt_print_modes =
-  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
+  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
 
 val _ = Outer_Syntax.improper_command "values" "enumerate and print comprehensions" Keyword.diag
   (opt_print_modes -- Scan.optional (Parse.nat >> SOME) NONE -- Parse.term
diff -r aae5566d6756 -r 94aa7b81bcf6 src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -221,15 +221,15 @@
 
 
 val opt_modes =
-  Scan.optional (Parse.$$$ "(" |-- Args.$$$ "modes" |-- Parse.$$$ ":" |--
-    (((Parse.enum1 "and" (Parse.xname --| Parse.$$$ ":" --
+  Scan.optional (@{keyword "("} |-- Args.$$$ "modes" |-- @{keyword ":"} |--
+    (((Parse.enum1 "and" (Parse.xname --| @{keyword ":"} --
         (Parse.enum "," mode_and_opt_proposal))) >> Multiple_Preds)
       || ((Parse.enum "," mode_and_opt_proposal) >> Single_Pred))
-    --| Parse.$$$ ")") (Multiple_Preds [])
+    --| @{keyword ")"}) (Multiple_Preds [])
 
 val opt_expected_modes =
-  Scan.optional (Parse.$$$ "(" |-- Args.$$$ "expected_modes" |-- Parse.$$$ ":" |--
-    Parse.enum "," parse_mode_expr --| Parse.$$$ ")" >> SOME) NONE
+  Scan.optional (@{keyword "("} |-- Args.$$$ "expected_modes" |-- @{keyword ":"} |--
+    Parse.enum "," parse_mode_expr --| @{keyword ")"} >> SOME) NONE
 
 (* Parser for options *)
 
@@ -238,18 +238,18 @@
     val scan_bool_option = foldl1 (op ||) (map Args.$$$ bool_options)
     val scan_compilation = foldl1 (op ||) (map (fn (s, c) => Args.$$$ s >> K c) compilation_names)
   in
-    Scan.optional (Parse.$$$ "[" |-- Scan.optional scan_compilation Pred
-      -- Parse.enum "," scan_bool_option --| Parse.$$$ "]")
+    Scan.optional (@{keyword "["} |-- Scan.optional scan_compilation Pred
+      -- Parse.enum "," scan_bool_option --| @{keyword "]"})
       (Pred, [])
   end
 
 val opt_print_modes =
-  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
+  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
 
-val opt_mode = (Parse.$$$ "_" >> K NONE) || (parse_mode_expr >> SOME)
+val opt_mode = (Args.$$$ "_" >> K NONE) || (parse_mode_expr >> SOME)
 
-val opt_param_modes = Scan.optional (Parse.$$$ "[" |-- Args.$$$ "mode" |-- Parse.$$$ ":" |--
-  Parse.enum ", " opt_mode --| Parse.$$$ "]" >> SOME) NONE
+val opt_param_modes = Scan.optional (@{keyword "["} |-- Args.$$$ "mode" |-- @{keyword ":"} |--
+  Parse.enum ", " opt_mode --| @{keyword "]"} >> SOME) NONE
 
 val stats = Scan.optional (Args.$$$ "stats" >> K true) false
 
@@ -264,7 +264,7 @@
         (Pred, [])
   in
     Scan.optional
-      (Parse.$$$ "[" |-- (expected_values -- stats) -- scan_compilation --| Parse.$$$ "]")
+      (@{keyword "["} |-- (expected_values -- stats) -- scan_compilation --| @{keyword "]"})
       ((NONE, false), (Pred, []))
   end
 
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)))
 
diff -r aae5566d6756 -r 94aa7b81bcf6 src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -109,7 +109,7 @@
 (* parser and command *)
 val quotdef_parser =
   Scan.option Parse_Spec.constdecl --
-    Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| Parse.$$$ "is" -- Parse.term))
+    Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| @{keyword "is"} -- Parse.term))
 
 val _ =
   Outer_Syntax.local_theory "quotient_definition"
diff -r aae5566d6756 -r 94aa7b81bcf6 src/HOL/Tools/Quotient/quotient_info.ML
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -71,7 +71,7 @@
 
 val quotmaps_attribute_setup =
   Attrib.setup @{binding map}
-    ((Args.type_name false --| Scan.lift (Parse.$$$ "=")) --  (* FIXME Args.type_name true (requires "set" type) *)
+    ((Args.type_name false --| Scan.lift (@{keyword "="})) --  (* FIXME Args.type_name true (requires "set" type) *)
       Args.const_proper true >>
       (fn (tyname, relname) =>
         let val minfo = {relmap = relname}
diff -r aae5566d6756 -r 94aa7b81bcf6 src/HOL/Tools/Quotient/quotient_type.ML
--- a/src/HOL/Tools/Quotient/quotient_type.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_type.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -262,15 +262,15 @@
     quotient_type spec' lthy
   end
 
-val partial = Scan.optional (Parse.reserved "partial" -- Parse.$$$ ":" >> K true) false
+val partial = Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false
 
 val quotspec_parser =
   Parse.and_list1
     ((Parse.type_args -- Parse.binding) --
       (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *)
-      Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) --
-        (Parse.$$$ "/" |-- (partial -- Parse.term))  --
-        Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding)))
+      Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --
+        (@{keyword "/"} |-- (partial -- Parse.term))  --
+        Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)))
 
 val _ =
   Outer_Syntax.local_theory_to_proof "quotient_type"
diff -r aae5566d6756 -r 94aa7b81bcf6 src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -86,7 +86,7 @@
     context
     |> Solvers.map (apfst (Symtab.update (name, (info, []))))
     |> Context.map_theory (Attrib.setup (Binding.name (name ^ "_options"))
-        (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
+        (Scan.lift (@{keyword "="} |-- Args.name) >>
           (Thm.declaration_attribute o K o set_solver_options o pair name))
         ("Additional command line options for SMT solver " ^ quote name))
 
@@ -142,7 +142,7 @@
 
 val setup_solver =
   Attrib.setup @{binding smt_solver}
-    (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
+    (Scan.lift (@{keyword "="} |-- Args.name) >>
       (Thm.declaration_attribute o K o select_solver))
     "SMT solver configuration"
 
@@ -207,7 +207,7 @@
 
 val setup_certificates =
   Attrib.setup @{binding smt_certificates}
-    (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
+    (Scan.lift (@{keyword "="} |-- Args.name) >>
       (Thm.declaration_attribute o K o select_certificates))
     "SMT certificates configuration"
 
diff -r aae5566d6756 -r 94aa7b81bcf6 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -396,12 +396,12 @@
                                        |> sort_strings |> cat_lines))
                   end))
 
-val parse_query_bang = Parse.$$$ "?" || Parse.$$$ "!" || Parse.$$$ "!!"
+val parse_query_bang = @{keyword "?"} || @{keyword "!"} || @{keyword "!!"}
 val parse_key =
   Scan.repeat1 (Parse.typ_group || parse_query_bang) >> implode_param
 val parse_value =
   Scan.repeat1 (Parse.xname || Parse.float_number || parse_query_bang)
-val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
+val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) []
 val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
 val parse_fact_refs =
   Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse_Spec.xthm)
diff -r aae5566d6756 -r 94aa7b81bcf6 src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/choice_specification.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -234,11 +234,11 @@
 
 (* outer syntax *)
 
-val opt_name = Scan.optional (Parse.name --| Parse.$$$ ":") ""
+val opt_name = Scan.optional (Parse.name --| @{keyword ":"}) ""
 val opt_overloaded = Parse.opt_keyword "overloaded"
 
 val specification_decl =
-  Parse.$$$ "(" |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| Parse.$$$ ")" --
+  @{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} --
           Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop)
 
 val _ =
@@ -249,7 +249,7 @@
 
 val ax_specification_decl =
     Parse.name --
-    (Parse.$$$ "(" |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| Parse.$$$ ")" --
+    (@{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} --
            Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop))
 
 val _ =
diff -r aae5566d6756 -r 94aa7b81bcf6 src/HOL/Tools/enriched_type.ML
--- a/src/HOL/Tools/enriched_type.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/enriched_type.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -268,7 +268,7 @@
 
 val _ = Outer_Syntax.local_theory_to_proof "enriched_type"
   "register operations managing the functorial structure of a type"
-  Keyword.thy_goal (Scan.option (Parse.name --| Parse.$$$ ":") -- Parse.term
+  Keyword.thy_goal (Scan.option (Parse.name --| @{keyword ":"}) -- Parse.term
     >> (fn (prfx, t) => enriched_type_cmd prfx t));
 
 end;
diff -r aae5566d6756 -r 94aa7b81bcf6 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/inductive.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -1137,7 +1137,7 @@
 fun gen_ind_decl mk_def coind =
   Parse.fixes -- Parse.for_fixes --
   Scan.optional Parse_Spec.where_alt_specs [] --
-  Scan.optional (Parse.$$$ "monos" |-- Parse.!!! Parse_Spec.xthms1) []
+  Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse_Spec.xthms1) []
   >> (fn (((preds, params), specs), monos) =>
       (snd oo gen_add_inductive mk_def true coind preds params specs monos));
 
diff -r aae5566d6756 -r 94aa7b81bcf6 src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/recdef.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -291,12 +291,12 @@
 (* outer syntax *)
 
 val hints =
-  Parse.$$$ "(" |--
-    Parse.!!! (Parse.position (Parse.$$$ "hints" -- Args.parse) --| Parse.$$$ ")") >> Args.src;
+  @{keyword "("} |--
+    Parse.!!! (Parse.position (@{keyword "hints"} -- Args.parse) --| @{keyword ")"}) >> Args.src;
 
 val recdef_decl =
   Scan.optional
-    (Parse.$$$ "(" -- Parse.!!! (Parse.$$$ "permissive" -- Parse.$$$ ")") >> K false) true --
+    (@{keyword "("} -- Parse.!!! (@{keyword "permissive"} -- @{keyword ")"}) >> K false) true --
   Parse.name -- Parse.term -- Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)
     -- Scan.option hints
   >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map Parse.triple_swap eqs) src);
@@ -309,7 +309,7 @@
 val defer_recdef_decl =
   Parse.name -- Scan.repeat1 Parse.prop --
   Scan.optional
-    (Parse.$$$ "(" |-- Parse.$$$ "congs" |-- Parse.!!! (Parse_Spec.xthms1 --| Parse.$$$ ")")) []
+    (@{keyword "("} |-- @{keyword "congs"} |-- Parse.!!! (Parse_Spec.xthms1 --| @{keyword ")"})) []
   >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
 
 val _ =
@@ -320,7 +320,7 @@
   Outer_Syntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
     Keyword.thy_goal
     ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.xname --
-        Scan.option (Parse.$$$ "(" |-- Parse.nat --| Parse.$$$ ")")
+        Scan.option (@{keyword "("} |-- Parse.nat --| @{keyword ")"})
       >> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
 
 end;
diff -r aae5566d6756 -r 94aa7b81bcf6 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/record.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -2313,7 +2313,7 @@
 val _ =
   Outer_Syntax.command "record" "define extensible record" Keyword.thy_decl
     (Parse.type_args_constrained -- Parse.binding --
-      (Parse.$$$ "=" |-- Scan.option (Parse.typ --| Parse.$$$ "+") --
+      (@{keyword "="} |-- Scan.option (Parse.typ --| @{keyword "+"}) --
         Scan.repeat1 Parse.const_binding)
     >> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd x y z)));
 
diff -r aae5566d6756 -r 94aa7b81bcf6 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/refute.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -3202,8 +3202,8 @@
 
 (*optional list of arguments of the form [name1=value1, name2=value2, ...]*)
 
-val scan_parm = Parse.name -- (Scan.optional (Parse.$$$ "=" |-- Parse.name) "true")
-val scan_parms = Scan.optional (Parse.$$$ "[" |-- Parse.list scan_parm --| Parse.$$$ "]") [];
+val scan_parm = Parse.name -- (Scan.optional (@{keyword "="} |-- Parse.name) "true")
+val scan_parms = Scan.optional (@{keyword "["} |-- Parse.list scan_parm --| @{keyword "]"}) [];
 
 
 (* 'refute' command *)
diff -r aae5566d6756 -r 94aa7b81bcf6 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/typedef.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -302,12 +302,12 @@
 val _ =
   Outer_Syntax.local_theory_to_proof "typedef" "HOL type definition (requires non-emptiness proof)"
     Keyword.thy_goal
-    (Scan.optional (Parse.$$$ "(" |--
-        ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
-          Parse.binding >> (fn s => (true, SOME s))) --| Parse.$$$ ")") (true, NONE) --
+    (Scan.optional (@{keyword "("} |--
+        ((@{keyword "open"} >> K false) -- Scan.option Parse.binding ||
+          Parse.binding >> (fn s => (true, SOME s))) --| @{keyword ")"}) (true, NONE) --
       (Parse.type_args_constrained -- Parse.binding) --
-        Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.term) --
-        Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding))
+        Parse.opt_mixfix -- (@{keyword "="} |-- Parse.term) --
+        Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
     >> (fn ((((((def, opt_name), (args, t)), mx), A), morphs)) =>
         typedef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs)));
 
diff -r aae5566d6756 -r 94aa7b81bcf6 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/Tools/Code/code_printer.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -394,13 +394,11 @@
     | _ => Scan.!! (err s) Scan.fail ()
   end;
 
-val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr");
-
 fun parse_syntax mk_plain mk_complex prep_arg =
   Scan.option (
-      ((Parse.$$$ infixK >> K X)
-        || (Parse.$$$ infixlK >> K L)
-        || (Parse.$$$ infixrK >> K R))
+      ((@{keyword "infix"} >> K X)
+        || (@{keyword "infixl"} >> K L)
+        || (@{keyword "infixr"} >> K R))
         -- Parse.nat -- Parse.string
         >> (fn ((x, i), s) => mk_complex (parse_infix prep_arg (x, i) s))
       || Parse.string >> (fn s => (parse_mixfix mk_plain mk_complex prep_arg s)));
diff -r aae5566d6756 -r 94aa7b81bcf6 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/Tools/Code/code_runtime.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -344,24 +344,19 @@
 
 local
 
-val datatypesK = "datatypes";
-val functionsK = "functions";
-val fileK = "file";
-val andK = "and"
-
 val parse_datatype =
-  Parse.name --| Parse.$$$ "=" --
+  Parse.name --| @{keyword "="} --
     (((Parse.sym_ident || Parse.string) >> (fn "_" => NONE | _ => Scan.fail ()))
-    || ((Parse.term ::: (Scan.repeat (Parse.$$$ "|" |-- Parse.term))) >> SOME));
+    || ((Parse.term ::: (Scan.repeat (@{keyword "|"} |-- Parse.term))) >> SOME));
 
 in
 
 val _ =
   Outer_Syntax.command "code_reflect" "enrich runtime environment with generated code"
-    Keyword.thy_decl (Parse.name -- Scan.optional (Parse.$$$ datatypesK |-- (parse_datatype
-      ::: Scan.repeat (Parse.$$$ andK |-- parse_datatype))) []
-    -- Scan.optional (Parse.$$$ functionsK |-- Scan.repeat1 Parse.name) []
-    -- Scan.option (Parse.$$$ fileK |-- Parse.name)
+    Keyword.thy_decl (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- (parse_datatype
+      ::: Scan.repeat (@{keyword "and"} |-- parse_datatype))) []
+    -- Scan.optional (@{keyword "functions"} |-- Scan.repeat1 Parse.name) []
+    -- Scan.option (@{keyword "file"} |-- Parse.name)
   >> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory
     (code_reflect_cmd raw_datatypes raw_functions module_name some_file)));
 
diff -r aae5566d6756 -r 94aa7b81bcf6 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/Tools/Code/code_target.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -638,8 +638,8 @@
 
 fun process_multi_syntax parse_thing parse_syntax change =
   (Parse.and_list1 parse_thing
-  :|-- (fn things => Scan.repeat1 (Parse.$$$ "(" |-- Parse.name --
-        (zip_list things parse_syntax (Parse.$$$ "and")) --| Parse.$$$ ")")))
+  :|-- (fn things => Scan.repeat1 (@{keyword "("} |-- Parse.name --
+        (zip_list things parse_syntax (@{keyword "and"})) --| @{keyword ")"})))
   >> (Toplevel.theory oo fold)
     (fn (target, syns) => fold (fn (raw_x, syn) => change target raw_x syn) syns);
 
@@ -667,18 +667,16 @@
 
 (** Isar setup **)
 
-val (inK, module_nameK, fileK, checkingK) = ("in", "module_name", "file", "checking");
-
-val code_expr_argsP = Scan.optional (Parse.$$$ "(" |-- Args.parse --| Parse.$$$ ")") [];
+val code_expr_argsP = Scan.optional (@{keyword "("} |-- Args.parse --| @{keyword ")"}) [];
 
 val code_exprP =
   Scan.repeat1 Parse.term_group :|-- (fn raw_cs =>
-    ((Parse.$$$ checkingK |-- Scan.repeat (Parse.name
-      -- ((Parse.$$$ "?" |-- Scan.succeed false) || Scan.succeed true) -- code_expr_argsP))
+    ((@{keyword "checking"} |-- Scan.repeat (Parse.name
+      -- ((@{keyword "?"} |-- Scan.succeed false) || Scan.succeed true) -- code_expr_argsP))
       >> (fn seris => check_code_cmd raw_cs seris)
-    || Scan.repeat (Parse.$$$ inK |-- Parse.name
-       -- Scan.optional (Parse.$$$ module_nameK |-- Parse.name) ""
-       -- Scan.optional (Parse.$$$ fileK |-- Parse.name) ""
+    || Scan.repeat (@{keyword "in"} |-- Parse.name
+       -- Scan.optional (@{keyword "module_name"} |-- Parse.name) ""
+       -- Scan.optional (@{keyword "file"} |-- Parse.name) ""
        -- code_expr_argsP) >> (fn seris => export_code_cmd raw_cs seris)));
 
 val _ =
@@ -688,7 +686,7 @@
 
 val _ =
   Outer_Syntax.command "code_instance" "define code syntax for instance" Keyword.thy_decl (
-    process_multi_syntax (Parse.xname --| Parse.$$$ "::" -- Parse.xname)
+    process_multi_syntax (Parse.xname --| @{keyword "::"} -- Parse.xname)
       (Scan.option (Parse.minus >> K ()))
     add_instance_syntax_cmd);
 
@@ -713,7 +711,7 @@
   Outer_Syntax.command "code_include" "declare piece of code to be included in generated code"
     Keyword.thy_decl (
     Parse.name -- Parse.name -- (Parse.text :|-- (fn "-" => Scan.succeed NONE
-      | s => Scan.optional (Parse.$$$ "attach" |-- Scan.repeat1 Parse.term) [] >> pair s >> SOME))
+      | s => Scan.optional (@{keyword "attach"} |-- Scan.repeat1 Parse.term) [] >> pair s >> SOME))
     >> (fn ((target, name), content_consts) =>
         (Toplevel.theory o add_include_cmd target) (name, content_consts))
   );
diff -r aae5566d6756 -r 94aa7b81bcf6 src/Tools/interpretation_with_defs.ML
--- a/src/Tools/interpretation_with_defs.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/Tools/interpretation_with_defs.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -83,8 +83,8 @@
   Outer_Syntax.command "interpretation"
     "prove interpretation of locale expression in theory" Keyword.thy_goal
     (Parse.!!! (Parse_Spec.locale_expression true) --
-      Scan.optional (Parse.$$$ "defines" |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
-        -- ((Parse.binding -- Parse.opt_mixfix') --| Parse.$$$ "is" -- Parse.term))) [] --
+      Scan.optional (@{keyword "defines"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
+        -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "is"} -- Parse.term))) [] --
       Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
       >> (fn ((expr, defs), equations) => Toplevel.print o
           Toplevel.theory_to_proof (interpretation_cmd expr defs equations)));
diff -r aae5566d6756 -r 94aa7b81bcf6 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/Tools/quickcheck.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -522,12 +522,12 @@
 
 val parse_arg =
   Parse.name --
-    (Scan.optional (Parse.$$$ "=" |--
+    (Scan.optional (@{keyword "="} |--
       (((Parse.name || Parse.float_number) >> single) ||
-        (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]"))) ["true"]);
+        (@{keyword "["} |-- Parse.list1 Parse.name --| @{keyword "]"}))) ["true"]);
 
 val parse_args =
-  Parse.$$$ "[" |-- Parse.list1 parse_arg --| Parse.$$$ "]" || Scan.succeed [];
+  @{keyword "["} |-- Parse.list1 parse_arg --| @{keyword "]"} || Scan.succeed [];
 
 val _ =
   Outer_Syntax.command quickcheck_paramsN "set parameters for random testing" Keyword.thy_decl
diff -r aae5566d6756 -r 94aa7b81bcf6 src/Tools/value.ML
--- a/src/Tools/value.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/Tools/value.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -57,10 +57,10 @@
   in Pretty.writeln p end;
 
 val opt_modes =
-  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
+  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
 
 val opt_evaluator =
-  Scan.option (Parse.$$$ "[" |-- Parse.xname --| Parse.$$$ "]")
+  Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"})
   
 val _ =
   Outer_Syntax.improper_command "value" "evaluate and print term" Keyword.diag
diff -r aae5566d6756 -r 94aa7b81bcf6 src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -427,15 +427,15 @@
   #1 o add_datatype (dom, map fst dts) (map snd dts) (monos, type_intrs, type_elims);
 
 val con_decl =
-  Parse.name -- Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.term --| Parse.$$$ ")") [] --
+  Parse.name -- Scan.optional (@{keyword "("} |-- Parse.list1 Parse.term --| @{keyword ")"}) [] --
     Parse.opt_mixfix >> Parse.triple1;
 
 val datatype_decl =
-  (Scan.optional ((Parse.$$$ "\<subseteq>" || Parse.$$$ "<=") |-- Parse.!!! Parse.term) "") --
-  Parse.and_list1 (Parse.term -- (Parse.$$$ "=" |-- Parse.enum1 "|" con_decl)) --
-  Scan.optional (Parse.$$$ "monos" |-- Parse.!!! Parse_Spec.xthms1) [] --
-  Scan.optional (Parse.$$$ "type_intros" |-- Parse.!!! Parse_Spec.xthms1) [] --
-  Scan.optional (Parse.$$$ "type_elims" |-- Parse.!!! Parse_Spec.xthms1) []
+  (Scan.optional ((@{keyword "\<subseteq>"} || @{keyword "<="}) |-- Parse.!!! Parse.term) "") --
+  Parse.and_list1 (Parse.term -- (@{keyword "="} |-- Parse.enum1 "|" con_decl)) --
+  Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse_Spec.xthms1) [] --
+  Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse_Spec.xthms1) [] --
+  Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse_Spec.xthms1) []
   >> (Toplevel.theory o mk_datatype);
 
 val coind_prefix = if coind then "co" else "";
diff -r aae5566d6756 -r 94aa7b81bcf6 src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/ZF/Tools/induct_tacs.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -189,10 +189,10 @@
 (* outer syntax *)
 
 val rep_datatype_decl =
-  (Parse.$$$ "elimination" |-- Parse.!!! Parse_Spec.xthm) --
-  (Parse.$$$ "induction" |-- Parse.!!! Parse_Spec.xthm) --
-  (Parse.$$$ "case_eqns" |-- Parse.!!! Parse_Spec.xthms1) --
-  Scan.optional (Parse.$$$ "recursor_eqns" |-- Parse.!!! Parse_Spec.xthms1) []
+  (@{keyword "elimination"} |-- Parse.!!! Parse_Spec.xthm) --
+  (@{keyword "induction"} |-- Parse.!!! Parse_Spec.xthm) --
+  (@{keyword "case_eqns"} |-- Parse.!!! Parse_Spec.xthms1) --
+  Scan.optional (@{keyword "recursor_eqns"} |-- Parse.!!! Parse_Spec.xthms1) []
   >> (fn (((x, y), z), w) => rep_datatype x y z w);
 
 val _ =
diff -r aae5566d6756 -r 94aa7b81bcf6 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -580,14 +580,14 @@
   #1 o add_inductive doms (map Parse.triple_swap intrs) (monos, con_defs, type_intrs, type_elims);
 
 val ind_decl =
-  (Parse.$$$ "domains" |-- Parse.!!! (Parse.enum1 "+" Parse.term --
-      ((Parse.$$$ "\<subseteq>" || Parse.$$$ "<=") |-- Parse.term))) --
-  (Parse.$$$ "intros" |--
+  (@{keyword "domains"} |-- Parse.!!! (Parse.enum1 "+" Parse.term --
+      ((@{keyword "\<subseteq>"} || @{keyword "<="}) |-- Parse.term))) --
+  (@{keyword "intros"} |--
     Parse.!!! (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop))) --
-  Scan.optional (Parse.$$$ "monos" |-- Parse.!!! Parse_Spec.xthms1) [] --
-  Scan.optional (Parse.$$$ "con_defs" |-- Parse.!!! Parse_Spec.xthms1) [] --
-  Scan.optional (Parse.$$$ "type_intros" |-- Parse.!!! Parse_Spec.xthms1) [] --
-  Scan.optional (Parse.$$$ "type_elims" |-- Parse.!!! Parse_Spec.xthms1) []
+  Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse_Spec.xthms1) [] --
+  Scan.optional (@{keyword "con_defs"} |-- Parse.!!! Parse_Spec.xthms1) [] --
+  Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse_Spec.xthms1) [] --
+  Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse_Spec.xthms1) []
   >> (Toplevel.theory o mk_ind);
 
 val _ =