# HG changeset patch
# User wenzelm
# Date 1331918482 -3600
# Node ID daf5538144d65f7b7258820acc8c37fe22885287
# Parent  0c8fb96cce73c029a0e485f01a0d2607af9c497d# Parent  5c6955f487e57080131bd1132f5e079690a26446
merged

diff -r 0c8fb96cce73 -r daf5538144d6 NEWS
--- a/NEWS	Fri Mar 16 16:32:34 2012 +0000
+++ b/NEWS	Fri Mar 16 18:21:22 2012 +0100
@@ -379,6 +379,10 @@
 * Antiquotation @{keyword "name"} produces a parser for outer syntax
 from a minor keyword introduced via theory header declaration.
 
+* Antiquotation @{command_spec "name"} produces the
+Outer_Syntax.command_spec from a major keyword introduced via theory
+header declaration; it can be passed to Outer_Syntax.command etc.
+
 * Local_Theory.define no longer hard-wires default theorem name
 "foo_def": definitional packages need to make this explicit, and may
 choose to omit theorem bindings for definitions by using
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Boogie/Tools/boogie_commands.ML
--- a/src/HOL/Boogie/Tools/boogie_commands.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -275,9 +275,8 @@
   (Parse.string --| Args.colon -- Parse.nat))) []
 
 val _ =
-  Outer_Syntax.command "boogie_open"
+  Outer_Syntax.command @{command_spec "boogie_open"}
     "open a new Boogie environment and load a Boogie-generated .b2i file"
-    Keyword.thy_decl
     (scan_opt "quiet" -- Parse.name -- vc_offsets >> 
       (Toplevel.theory o boogie_open))
 
@@ -303,9 +302,8 @@
   Scan.succeed VC_Complete
 
 val _ =
-  Outer_Syntax.command "boogie_vc"
+  Outer_Syntax.command @{command_spec "boogie_vc"}
     "enter into proof mode for a specific verification condition"
-    Keyword.thy_goal
     (vc_name -- vc_opts >> (fn args =>
       (Toplevel.print o Toplevel.theory_to_proof (boogie_vc args))))
 
@@ -336,18 +334,16 @@
   f (Toplevel.theory_of state))
 
 val _ =
-  Outer_Syntax.improper_command "boogie_status"
+  Outer_Syntax.improper_command @{command_spec "boogie_status"}
     "show the name and state of all loaded verification conditions"
-    Keyword.diag
     (status_test >> status_cmd ||
      status_vc >> status_cmd ||
      Scan.succeed (status_cmd boogie_status))
 
 
 val _ =
-  Outer_Syntax.command "boogie_end"
+  Outer_Syntax.command @{command_spec "boogie_end"}
     "close the current Boogie environment"
-    Keyword.thy_decl
     (Scan.succeed (Toplevel.theory boogie_end))
 
 
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/HOLCF/Tools/Domain/domain.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/HOLCF/Tools/Domain/domain.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -262,7 +262,7 @@
   end
 
 val _ =
-  Outer_Syntax.command "domain" "define recursive domains (HOLCF)"
-    Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain))
+  Outer_Syntax.command @{command_spec "domain"} "define recursive domains (HOLCF)"
+    (domains_decl >> (Toplevel.theory o mk_domain))
 
 end
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -771,8 +771,7 @@
 in
 
 val _ =
-  Outer_Syntax.command "domain_isomorphism" "define domain isomorphisms (HOLCF)"
-    Keyword.thy_decl
+  Outer_Syntax.command @{command_spec "domain_isomorphism"} "define domain isomorphisms (HOLCF)"
     (parse_domain_isos >> (Toplevel.theory o domain_isomorphism_cmd))
 
 end
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/HOLCF/Tools/cpodef.ML
--- a/src/HOL/HOLCF/Tools/cpodef.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/HOLCF/Tools/cpodef.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -357,14 +357,14 @@
     ((def, the_default t opt_name), (t, args, mx), A, morphs)
 
 val _ =
-  Outer_Syntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)"
-  Keyword.thy_goal
+  Outer_Syntax.command @{command_spec "pcpodef"}
+    "HOLCF type definition (requires admissibility proof)"
     (typedef_proof_decl >>
       (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)))
 
 val _ =
-  Outer_Syntax.command "cpodef" "HOLCF type definition (requires admissibility proof)"
-  Keyword.thy_goal
+  Outer_Syntax.command @{command_spec "cpodef"}
+    "HOLCF type definition (requires admissibility proof)"
     (typedef_proof_decl >>
       (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)))
 
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/HOLCF/Tools/domaindef.ML
--- a/src/HOL/HOLCF/Tools/domaindef.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/HOLCF/Tools/domaindef.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -224,7 +224,7 @@
   domaindef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs)
 
 val _ =
-  Outer_Syntax.command "domaindef" "HOLCF definition of domains from deflations" Keyword.thy_decl
+  Outer_Syntax.command @{command_spec "domaindef"} "HOLCF definition of domains from deflations"
     (domaindef_decl >>
       (Toplevel.print oo (Toplevel.theory o mk_domaindef)))
 
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/HOLCF/Tools/fixrec.ML
--- a/src/HOL/HOLCF/Tools/fixrec.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/HOLCF/Tools/fixrec.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -402,7 +402,7 @@
   in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! (@{keyword "|"}))) end
 
 val _ =
-  Outer_Syntax.local_theory "fixrec" "define recursive functions (HOLCF)" Keyword.thy_decl
+  Outer_Syntax.local_theory @{command_spec "fixrec"} "define recursive functions (HOLCF)"
     (Parse.fixes -- (Parse.where_ |-- Parse.!!! alt_specs')
       >> (fn (fixes, specs) => add_fixrec_cmd fixes specs))
 
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Import/import.ML
--- a/src/HOL/Import/import.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Import/import.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -238,51 +238,43 @@
 val append_dump = (Parse.verbatim || Parse.string) >> add_dump
 
 val _ =
-  (Outer_Syntax.command "import_segment"
-                       "Set import segment name"
-                       Keyword.thy_decl (import_segment >> Toplevel.theory);
-   Outer_Syntax.command "import_theory"
-                       "Set default external theory name"
-                       Keyword.thy_decl (import_theory >> Toplevel.theory);
-   Outer_Syntax.command "end_import"
-                       "End external import"
-                       Keyword.thy_decl (end_import >> Toplevel.theory);
-   Outer_Syntax.command "setup_theory"
-                       "Setup external theory replaying"
-                       Keyword.thy_decl (setup_theory >> Toplevel.theory);
-   Outer_Syntax.command "end_setup"
-                       "End external setup"
-                       Keyword.thy_decl (end_setup >> Toplevel.theory);
-   Outer_Syntax.command "setup_dump"
-                       "Setup the dump file name"
-                       Keyword.thy_decl (set_dump >> Toplevel.theory);
-   Outer_Syntax.command "append_dump"
-                       "Add text to dump file"
-                       Keyword.thy_decl (append_dump >> Toplevel.theory);
-   Outer_Syntax.command "flush_dump"
-                       "Write the dump to file"
-                       Keyword.thy_decl (fl_dump >> Toplevel.theory);
-   Outer_Syntax.command "ignore_thms"
-                       "Theorems to ignore in next external theory import"
-                       Keyword.thy_decl (ignore_thms >> Toplevel.theory);
-   Outer_Syntax.command "type_maps"
-                       "Map external type names to existing Isabelle/HOL type names"
-                       Keyword.thy_decl (type_maps >> Toplevel.theory);
-   Outer_Syntax.command "def_maps"
-                       "Map external constant names to their primitive definitions"
-                       Keyword.thy_decl (def_maps >> Toplevel.theory);
-   Outer_Syntax.command "thm_maps"
-                       "Map external theorem names to existing Isabelle/HOL theorem names"
-                       Keyword.thy_decl (thm_maps >> Toplevel.theory);
-   Outer_Syntax.command "const_renames"
-                       "Rename external const names"
-                       Keyword.thy_decl (const_renames >> Toplevel.theory);
-   Outer_Syntax.command "const_moves"
-                       "Rename external const names to other external constants"
-                       Keyword.thy_decl (const_moves >> Toplevel.theory);
-   Outer_Syntax.command "const_maps"
-                       "Map external const names to existing Isabelle/HOL const names"
-                       Keyword.thy_decl (const_maps >> Toplevel.theory));
+  (Outer_Syntax.command @{command_spec "import_segment"} "set import segment name"
+     (import_segment >> Toplevel.theory);
+   Outer_Syntax.command @{command_spec "import_theory"} "set default external theory name"
+     (import_theory >> Toplevel.theory);
+   Outer_Syntax.command @{command_spec "end_import"} "end external import"
+     (end_import >> Toplevel.theory);
+   Outer_Syntax.command @{command_spec "setup_theory"} "setup external theory replaying"
+     (setup_theory >> Toplevel.theory);
+   Outer_Syntax.command @{command_spec "end_setup"} "end external setup"
+     (end_setup >> Toplevel.theory);
+   Outer_Syntax.command @{command_spec "setup_dump"} "setup the dump file name"
+     (set_dump >> Toplevel.theory);
+   Outer_Syntax.command @{command_spec "append_dump"} "add text to dump file"
+     (append_dump >> Toplevel.theory);
+   Outer_Syntax.command @{command_spec "flush_dump"} "write the dump to file"
+     (fl_dump >> Toplevel.theory);
+   Outer_Syntax.command @{command_spec "ignore_thms"}
+     "theorems to ignore in next external theory import"
+     (ignore_thms >> Toplevel.theory);
+   Outer_Syntax.command @{command_spec "type_maps"}
+     "map external type names to existing Isabelle/HOL type names"
+     (type_maps >> Toplevel.theory);
+   Outer_Syntax.command @{command_spec "def_maps"}
+     "map external constant names to their primitive definitions"
+     (def_maps >> Toplevel.theory);
+   Outer_Syntax.command @{command_spec "thm_maps"}
+     "map external theorem names to existing Isabelle/HOL theorem names"
+     (thm_maps >> Toplevel.theory);
+   Outer_Syntax.command @{command_spec "const_renames"}
+     "rename external const names"
+     (const_renames >> Toplevel.theory);
+   Outer_Syntax.command @{command_spec "const_moves"}
+     "rename external const names to other external constants"
+     (const_moves >> Toplevel.theory);
+   Outer_Syntax.command @{command_spec "const_maps"}
+     "map external const names to existing Isabelle/HOL const names"
+     (const_maps >> Toplevel.theory));
 
 end
 
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Nominal/nominal_atoms.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -1016,7 +1016,7 @@
 (* syntax und parsing *)
 
 val _ =
-  Outer_Syntax.command "atom_decl" "declare new kinds of atoms" Keyword.thy_decl
+  Outer_Syntax.command @{command_spec "atom_decl"} "declare new kinds of atoms"
     (Scan.repeat1 Parse.name >> (Toplevel.theory o create_nom_typedecls));
 
 end;
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -2044,7 +2044,7 @@
 val nominal_datatype_cmd = gen_nominal_datatype Datatype.read_specs;
 
 val _ =
-  Outer_Syntax.command "nominal_datatype" "define nominal datatypes" Keyword.thy_decl
+  Outer_Syntax.command @{command_spec "nominal_datatype"} "define nominal datatypes"
     (Parse.and_list1 Datatype.spec_cmd >>
       (Toplevel.theory o nominal_datatype_cmd Datatype.default_config));
 
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -670,16 +670,15 @@
 (* outer syntax *)
 
 val _ =
-  Outer_Syntax.local_theory_to_proof "nominal_inductive"
+  Outer_Syntax.local_theory_to_proof @{command_spec "nominal_inductive"}
     "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes"
-    Keyword.thy_goal
     (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
+  Outer_Syntax.local_theory @{command_spec "equivariance"}
+    "prove equivariance for inductive predicate involving nominal datatypes"
     (Parse.xname -- Scan.optional (@{keyword "["} |-- Parse.list1 Parse.name --| @{keyword "]"}) [] >>
       (fn (name, atoms) => prove_eqvt name atoms));
 
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -484,9 +484,8 @@
 (* outer syntax *)
 
 val _ =
-  Outer_Syntax.local_theory_to_proof "nominal_inductive2"
+  Outer_Syntax.local_theory_to_proof @{command_spec "nominal_inductive2"}
     "prove strong induction theorem for inductive predicate involving nominal datatypes"
-    Keyword.thy_goal
     (Parse.xname -- 
      Scan.option (@{keyword "("} |-- Parse.!!! (Parse.name --| @{keyword ")"})) --
      (Scan.optional (@{keyword "avoids"} |-- Parse.enum1 "|" (Parse.name --
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Nominal/nominal_primrec.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -402,8 +402,8 @@
   Scan.optional (@{keyword "("} |-- Parse.!!! (parser2 --| @{keyword ")"})) (NONE, NONE);
 
 val _ =
-  Outer_Syntax.local_theory_to_proof "nominal_primrec"
-    "define primitive recursive functions on nominal datatypes" Keyword.thy_goal
+  Outer_Syntax.local_theory_to_proof @{command_spec "nominal_primrec"}
+    "define primitive recursive functions on nominal datatypes"
     (options -- Parse.fixes -- Parse.for_fixes -- Parse_Spec.where_alt_specs
       >> (fn ((((invs, fctxt), fixes), params), specs) =>
         add_primrec_cmd invs fctxt fixes params specs));
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Orderings.thy	Fri Mar 16 18:21:22 2012 +0100
@@ -409,8 +409,8 @@
 (** Diagnostic command **)
 
 val _ =
-  Outer_Syntax.improper_command "print_orders"
-    "print order structures available to transitivity reasoner" Keyword.diag
+  Outer_Syntax.improper_command @{command_spec "print_orders"}
+    "print order structures available to transitivity reasoner"
     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
         Toplevel.keep (print_structures o Toplevel.context_of)));
 
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -105,41 +105,36 @@
   end);
 
 val _ =
-  Outer_Syntax.command "spark_open"
+  Outer_Syntax.command @{command_spec "spark_open"}
     "open a new SPARK environment and load a SPARK-generated .vcg or .siv file"
-    Keyword.thy_decl
     (Parse.name -- Parse.parname >> (Toplevel.theory o spark_open));
 
 val pfun_type = Scan.option
   (Args.parens (Parse.list1 Parse.name) --| Args.colon -- Parse.name);
 
 val _ =
-  Outer_Syntax.command "spark_proof_functions"
+  Outer_Syntax.command @{command_spec "spark_proof_functions"}
     "associate SPARK proof functions with terms"
-    Keyword.thy_decl
     (Scan.repeat1 (Parse.name -- (pfun_type --| Args.$$$ "=" -- Parse.term)) >>
-       (Toplevel.theory o fold add_proof_fun_cmd));
+      (Toplevel.theory o fold add_proof_fun_cmd));
 
 val _ =
-  Outer_Syntax.command "spark_types"
+  Outer_Syntax.command @{command_spec "spark_types"}
     "associate SPARK types with types"
-    Keyword.thy_decl
     (Scan.repeat1 (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.typ --
        Scan.optional (Args.parens (Parse.list1
          (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.xname)))) [])) >>
        (Toplevel.theory o fold add_spark_type_cmd));
 
 val _ =
-  Outer_Syntax.command "spark_vc"
+  Outer_Syntax.command @{command_spec "spark_vc"}
     "enter into proof mode for a specific verification condition"
-    Keyword.thy_goal
     (Parse.name >> (fn name =>
       (Toplevel.print o Toplevel.local_theory_to_proof NONE (prove_vc name))));
 
 val _ =
-  Outer_Syntax.improper_command "spark_status"
+  Outer_Syntax.improper_command @{command_spec "spark_status"}
     "show the name and state of all loaded verification conditions"
-    Keyword.diag
     (Scan.optional
        (Args.parens
           (   Args.$$$ "proved" >> K (is_some, K "")
@@ -147,9 +142,8 @@
        (K true, string_of_status) >> show_status);
 
 val _ =
-  Outer_Syntax.command "spark_end"
+  Outer_Syntax.command @{command_spec "spark_end"}
     "close the current SPARK environment"
-    Keyword.thy_decl
     (Scan.succeed (Toplevel.theory SPARK_VCs.close));
 
 val setup = Theory.at_end (fn thy =>
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Statespace/state_space.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -699,7 +699,7 @@
         (plus1_unless comp parent --
           Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 comp)) [])));
 val _ =
-  Outer_Syntax.command "statespace" "define state space" Keyword.thy_decl
+  Outer_Syntax.command @{command_spec "statespace"} "define state space"
     (statespace_decl >> (fn ((args, name), (parents, comps)) =>
       Toplevel.theory (define_statespace args name parents comps)));
 
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -887,7 +887,7 @@
   in TPTP_Data.map (cons ((prob_name, result))) thy' end
 
 val _ =
-  Outer_Syntax.improper_command "import_tptp" "import TPTP problem" Keyword.thy_decl
+  Outer_Syntax.improper_command @{command_spec "import_tptp"} "import TPTP problem"
     (Parse.path >> (fn path =>
       Toplevel.theory (fn thy => import_file true (Path.dir path) path [] [] thy)))
 
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -792,7 +792,7 @@
   >> (fn (((vs, t), mx), cons) => ((t, vs, mx), map Parse.triple1 cons));
 
 val _ =
-  Outer_Syntax.command "datatype" "define inductive datatypes" Keyword.thy_decl
+  Outer_Syntax.command @{command_spec "datatype"} "define inductive datatypes"
     (Parse.and_list1 spec_cmd
       >> (Toplevel.theory o (snd oo add_datatype_cmd Datatype_Aux.default_config)));
 
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Tools/Datatype/primrec.ML
--- a/src/HOL/Tools/Datatype/primrec.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/Datatype/primrec.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -310,8 +310,8 @@
 (* outer syntax *)
 
 val _ =
-  Outer_Syntax.local_theory "primrec" "define primitive recursive functions on datatypes"
-    Keyword.thy_decl
+  Outer_Syntax.local_theory @{command_spec "primrec"}
+    "define primitive recursive functions on datatypes"
     (Parse.fixes -- Parse_Spec.where_alt_specs
       >> (fn (fixes, specs) => add_primrec_cmd fixes specs #> snd));
 
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Tools/Datatype/rep_datatype.ML
--- a/src/HOL/Tools/Datatype/rep_datatype.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -643,7 +643,7 @@
 (* outer syntax *)
 
 val _ =
-  Outer_Syntax.command "rep_datatype" "represent existing types inductively" Keyword.thy_goal
+  Outer_Syntax.command @{command_spec "rep_datatype"} "represent existing types inductively"
     (Scan.repeat1 Parse.term >> (fn ts =>
       Toplevel.print o
       Toplevel.theory_to_proof (rep_datatype_cmd Datatype_Aux.default_config (K I) ts)));
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Tools/Function/fun.ML
--- a/src/HOL/Tools/Function/fun.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/Function/fun.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -170,9 +170,9 @@
 
 
 val _ =
-  Outer_Syntax.local_theory' "fun" "define general recursive functions (short version)"
-  Keyword.thy_decl
-  (function_parser fun_config
-     >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config))
+  Outer_Syntax.local_theory' @{command_spec "fun"}
+    "define general recursive functions (short version)"
+    (function_parser fun_config
+      >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config))
 
 end
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/Function/function.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -277,15 +277,15 @@
 (* outer syntax *)
 
 val _ =
-  Outer_Syntax.local_theory_to_proof' "function" "define general recursive functions"
-  Keyword.thy_goal
-  (function_parser default_config
-     >> (fn ((config, fixes), statements) => function_cmd fixes statements config))
+  Outer_Syntax.local_theory_to_proof' @{command_spec "function"}
+    "define general recursive functions"
+    (function_parser default_config
+      >> (fn ((config, fixes), statements) => function_cmd fixes statements config))
 
 val _ =
-  Outer_Syntax.local_theory_to_proof "termination" "prove termination of a recursive function"
-  Keyword.thy_goal
-  (Scan.option Parse.term >> termination_cmd)
+  Outer_Syntax.local_theory_to_proof @{command_spec "termination"}
+    "prove termination of a recursive function"
+    (Scan.option Parse.term >> termination_cmd)
 
 
 end
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/Function/partial_function.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -281,10 +281,10 @@
 
 val mode = @{keyword "("} |-- Parse.xname --| @{keyword ")"};
 
-val _ = Outer_Syntax.local_theory
-  "partial_function" "define partial function" Keyword.thy_decl
-  ((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.spec)))
-     >> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec));
+val _ =
+  Outer_Syntax.local_theory @{command_spec "partial_function"} "define partial function"
+    ((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.spec)))
+      >> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec));
 
 
 val setup = Mono_Rules.setup;
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -390,16 +390,15 @@
                                params |> map string_for_raw_param
                                       |> sort_strings |> cat_lines)))))
 
-val parse_nitpick_command =
-  (parse_params -- Scan.optional Parse.nat 1) #>> nitpick_trans
-val parse_nitpick_params_command = parse_params #>> nitpick_params_trans
+val _ =
+  Outer_Syntax.improper_command @{command_spec "nitpick"}
+    "try to find a counterexample for a given subgoal using Nitpick"
+    ((parse_params -- Scan.optional Parse.nat 1) #>> nitpick_trans)
 
-val _ = Outer_Syntax.improper_command nitpickN
-            "try to find a counterexample for a given subgoal using Nitpick"
-            Keyword.diag parse_nitpick_command
-val _ = Outer_Syntax.command nitpick_paramsN
-            "set and display the default parameters for Nitpick"
-            Keyword.thy_decl parse_nitpick_params_command
+val _ =
+  Outer_Syntax.command @{command_spec "nitpick_params"}
+    "set and display the default parameters for Nitpick"
+    (parse_params #>> nitpick_params_trans)
 
 fun try_nitpick auto = pick_nits [] (if auto then Auto_Try else Try) 1 0
 
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -1004,10 +1004,13 @@
 val opt_print_modes =
   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
-   >> (fn ((print_modes, soln), t) => Toplevel.keep
-        (values_cmd print_modes soln t))); (*FIXME does not preserve the previous functionality*)
+val _ =
+  Outer_Syntax.improper_command @{command_spec "values"}
+    "enumerate and print comprehensions"
+    (opt_print_modes -- Scan.optional (Parse.nat >> SOME) NONE -- Parse.term
+     >> (fn ((print_modes, soln), t) => Toplevel.keep
+          (values_cmd print_modes soln t))); (*FIXME does not preserve the previous functionality*)
+
 
 (* quickcheck generator *)
 
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -270,14 +270,16 @@
 
 (* code_pred command and values command *)
 
-val _ = Outer_Syntax.local_theory_to_proof "code_pred"
-  "prove equations for predicate specified by intro/elim rules"
-  Keyword.thy_goal
-  (opt_expected_modes -- opt_modes -- scan_options -- Parse.term_group >> code_pred_cmd)
+val _ =
+  Outer_Syntax.local_theory_to_proof @{command_spec "code_pred"}
+    "prove equations for predicate specified by intro/elim rules"
+    (opt_expected_modes -- opt_modes -- scan_options -- Parse.term_group >> code_pred_cmd)
 
-val _ = Outer_Syntax.improper_command "values" "enumerate and print comprehensions" Keyword.diag
-  (opt_print_modes -- opt_param_modes -- value_options -- Scan.optional Parse.nat ~1 -- Parse.term
-    >> (fn ((((print_modes, param_modes), options), k), t) => Toplevel.keep
-        (Predicate_Compile_Core.values_cmd print_modes param_modes options k t)));
+val _ =
+  Outer_Syntax.improper_command @{command_spec "values"}
+    "enumerate and print comprehensions"
+    (opt_print_modes -- opt_param_modes -- value_options -- Scan.optional Parse.nat ~1 -- Parse.term
+      >> (fn ((((print_modes, param_modes), options), k), t) => Toplevel.keep
+          (Predicate_Compile_Core.values_cmd print_modes param_modes options k t)))
 
 end
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Tools/Quickcheck/abstract_generators.ML
--- a/src/HOL/Tools/Quickcheck/abstract_generators.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -64,8 +64,10 @@
 val quickcheck_generator_cmd = gen_quickcheck_generator
   (fn ctxt => fst o dest_Type o Proof_Context.read_type_name_proper ctxt false) Syntax.read_term
   
-val _ = Outer_Syntax.command "quickcheck_generator" "define quickcheck generators for abstract types"
-    Keyword.thy_decl ((Parse.type_const --
+val _ =
+  Outer_Syntax.command @{command_spec "quickcheck_generator"}
+    "define quickcheck generators for abstract types"
+    ((Parse.type_const --
       Scan.option (Args.$$$ "predicate" |-- @{keyword ":"} |-- Parse.term)) --
       (Args.$$$ "constructors" |-- @{keyword ":"} |-- Parse.list1 Parse.term)
       >> (fn ((tyco, opt_pred), constrs) =>
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Tools/Quickcheck/find_unused_assms.ML
--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -104,8 +104,8 @@
 
 
 val _ =
-  Outer_Syntax.improper_command "find_unused_assms" "find theorems with superfluous assumptions"
-    Keyword.diag
+  Outer_Syntax.improper_command @{command_spec "find_unused_assms"}
+    "find theorems with superfluous assumptions"
     (Scan.option Parse.name
       >> (fn opt_thy_name =>
         Toplevel.no_timing o Toplevel.keep (fn state =>
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -106,14 +106,13 @@
     quotient_def (SOME (Binding.name qconst_name, NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt
   end
 
-(* parser and command *)
-val quotdef_parser =
-  Scan.option Parse_Spec.constdecl --
-    Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| @{keyword "is"} -- Parse.term))
+(* command *)
 
 val _ =
-  Outer_Syntax.local_theory "quotient_definition"
+  Outer_Syntax.local_theory @{command_spec "quotient_definition"}
     "definition for constants over the quotient type"
-      Keyword.thy_decl (quotdef_parser >> (snd oo quotient_def_cmd))
+    (Scan.option Parse_Spec.constdecl --
+      Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| @{keyword "is"} -- Parse.term))
+      >> (snd oo quotient_def_cmd))
 
 end; (* structure *)
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Tools/Quotient/quotient_info.ML
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -291,15 +291,15 @@
 (* outer syntax commands *)
 
 val _ =
-  Outer_Syntax.improper_command "print_quotmaps" "print quotient map functions" Keyword.diag
+  Outer_Syntax.improper_command @{command_spec "print_quotmaps"} "print quotient map functions"
     (Scan.succeed (Toplevel.keep (print_quotmaps o Toplevel.context_of)))
 
 val _ =
-  Outer_Syntax.improper_command "print_quotients" "print quotients" Keyword.diag
+  Outer_Syntax.improper_command @{command_spec "print_quotients"} "print quotients"
     (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
 
 val _ =
-  Outer_Syntax.improper_command "print_quotconsts" "print quotient constants" Keyword.diag
+  Outer_Syntax.improper_command @{command_spec "print_quotconsts"} "print quotient constants"
     (Scan.succeed (Toplevel.keep (print_quotconsts o Toplevel.context_of)))
 
 end;
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Tools/Quotient/quotient_type.ML
--- a/src/HOL/Tools/Quotient/quotient_type.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/Quotient/quotient_type.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -264,17 +264,15 @@
 
 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 -- (@{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"
+  Outer_Syntax.local_theory_to_proof @{command_spec "quotient_type"}
     "quotient type definitions (require equivalence proofs)"
-       Keyword.thy_goal (quotspec_parser >> quotient_type_cmd)
+    (Parse.and_list1
+      ((Parse.type_args -- Parse.binding) --
+        (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *)
+        Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --
+          (@{keyword "/"} |-- (partial -- Parse.term))  --
+          Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)))
+    >> quotient_type_cmd)
 
 end;
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/SMT/smt_config.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -247,10 +247,9 @@
   end
 
 val _ =
-  Outer_Syntax.improper_command "smt_status"
-    ("show the available SMT solvers, the currently selected SMT solver, " ^
-      "and the values of SMT configuration options")
-    Keyword.diag
+  Outer_Syntax.improper_command @{command_spec "smt_status"}
+    "show the available SMT solvers, the currently selected SMT solver, \
+    \and the values of SMT configuration options"
     (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
       print_setup (Toplevel.context_of state))))
 
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -413,20 +413,16 @@
   Scan.optional (Args.parens (Scan.repeat parse_relevance_chunk
                               >> merge_relevance_overrides))
                 no_relevance_override
-val parse_sledgehammer_command =
-  (Scan.optional Parse.short_ident runN -- parse_params
-   -- parse_relevance_override -- Scan.option Parse.nat) #>> sledgehammer_trans
-val parse_sledgehammer_params_command =
-  parse_params #>> sledgehammer_params_trans
 
 val _ =
-  Outer_Syntax.improper_command sledgehammerN
-      "search for first-order proof using automatic theorem provers" Keyword.diag
-      parse_sledgehammer_command
+  Outer_Syntax.improper_command @{command_spec "sledgehammer"}
+    "search for first-order proof using automatic theorem provers"
+    ((Scan.optional Parse.short_ident runN -- parse_params
+      -- parse_relevance_override -- Scan.option Parse.nat) #>> sledgehammer_trans)
 val _ =
-  Outer_Syntax.command sledgehammer_paramsN
-      "set and display the default parameters for Sledgehammer" Keyword.thy_decl
-      parse_sledgehammer_params_command
+  Outer_Syntax.command @{command_spec "sledgehammer_params"}
+    "set and display the default parameters for Sledgehammer"
+    (parse_params #>> sledgehammer_params_trans)
 
 fun try_sledgehammer auto state =
   let
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/choice_specification.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -237,25 +237,19 @@
 val opt_name = Scan.optional (Parse.name --| @{keyword ":"}) ""
 val opt_overloaded = Parse.opt_keyword "overloaded"
 
-val specification_decl =
-  @{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} --
-          Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop)
+val _ =
+  Outer_Syntax.command @{command_spec "specification"} "define constants by specification"
+    (@{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} --
+      Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop)
+      >> (fn (cos, alt_props) => Toplevel.print o
+          (Toplevel.theory_to_proof (process_spec NONE cos alt_props))))
 
 val _ =
-  Outer_Syntax.command "specification" "define constants by specification" Keyword.thy_goal
-    (specification_decl >> (fn (cos,alt_props) =>
-                               Toplevel.print o (Toplevel.theory_to_proof
-                                                     (process_spec NONE cos alt_props))))
-
-val ax_specification_decl =
-    Parse.name --
-    (@{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} --
-           Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop))
-
-val _ =
-  Outer_Syntax.command "ax_specification" "define constants by specification" Keyword.thy_goal
-    (ax_specification_decl >> (fn (axname,(cos,alt_props)) =>
-                               Toplevel.print o (Toplevel.theory_to_proof
-                                                     (process_spec (SOME axname) cos alt_props))))
+  Outer_Syntax.command @{command_spec "ax_specification"} "define constants by specification"
+    (Parse.name --
+      (@{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} --
+        Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop))
+      >> (fn (axname, (cos, alt_props)) =>
+           Toplevel.print o (Toplevel.theory_to_proof (process_spec (SOME axname) cos alt_props))))
 
 end
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Tools/enriched_type.ML
--- a/src/HOL/Tools/enriched_type.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/enriched_type.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -266,9 +266,10 @@
 val enriched_type = gen_enriched_type Syntax.check_term;
 val enriched_type_cmd = gen_enriched_type Syntax.read_term;
 
-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 --| @{keyword ":"}) -- Parse.term
-    >> (fn (prfx, t) => enriched_type_cmd prfx t));
+val _ =
+  Outer_Syntax.local_theory_to_proof @{command_spec "enriched_type"}
+    "register operations managing the functorial structure of a type"
+    (Scan.option (Parse.name --| @{keyword ":"}) -- Parse.term
+      >> (fn (prfx, t) => enriched_type_cmd prfx t));
 
 end;
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/inductive.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -1144,21 +1144,21 @@
 val ind_decl = gen_ind_decl add_ind_def;
 
 val _ =
-  Outer_Syntax.local_theory' "inductive" "define inductive predicates" Keyword.thy_decl
+  Outer_Syntax.local_theory' @{command_spec "inductive"} "define inductive predicates"
     (ind_decl false);
 
 val _ =
-  Outer_Syntax.local_theory' "coinductive" "define coinductive predicates" Keyword.thy_decl
+  Outer_Syntax.local_theory' @{command_spec "coinductive"} "define coinductive predicates"
     (ind_decl true);
 
 val _ =
-  Outer_Syntax.local_theory "inductive_cases"
-    "create simplified instances of elimination rules (improper)" Keyword.thy_script
+  Outer_Syntax.local_theory @{command_spec "inductive_cases"}
+    "create simplified instances of elimination rules (improper)"
     (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
 
 val _ =
-  Outer_Syntax.local_theory "inductive_simps"
-    "create simplification rules for inductive predicates" Keyword.thy_script
+  Outer_Syntax.local_theory @{command_spec "inductive_simps"}
+    "create simplification rules for inductive predicates"
     (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_simps));
 
 end;
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/inductive_set.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -575,11 +575,11 @@
 val ind_set_decl = Inductive.gen_ind_decl add_ind_set_def;
 
 val _ =
-  Outer_Syntax.local_theory' "inductive_set" "define inductive sets" Keyword.thy_decl
+  Outer_Syntax.local_theory' @{command_spec "inductive_set"} "define inductive sets"
     (ind_set_decl false);
 
 val _ =
-  Outer_Syntax.local_theory' "coinductive_set" "define coinductive sets" Keyword.thy_decl
+  Outer_Syntax.local_theory' @{command_spec "coinductive_set"} "define coinductive sets"
     (ind_set_decl true);
 
 end;
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/recdef.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -302,7 +302,7 @@
   >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map Parse.triple_swap eqs) src);
 
 val _ =
-  Outer_Syntax.command "recdef" "define general recursive functions (TFL)" Keyword.thy_decl
+  Outer_Syntax.command @{command_spec "recdef"} "define general recursive functions (TFL)"
     (recdef_decl >> Toplevel.theory);
 
 
@@ -313,12 +313,13 @@
   >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
 
 val _ =
-  Outer_Syntax.command "defer_recdef" "defer general recursive functions (TFL)" Keyword.thy_decl
+  Outer_Syntax.command @{command_spec "defer_recdef"}
+    "defer general recursive functions (TFL)"
     (defer_recdef_decl >> Toplevel.theory);
 
 val _ =
-  Outer_Syntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
-    Keyword.thy_goal
+  Outer_Syntax.local_theory_to_proof' @{command_spec "recdef_tc"}
+    "recommence proof of termination condition (TFL)"
     ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.xname --
         Scan.option (@{keyword "("} |-- Parse.nat --| @{keyword ")"})
       >> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/record.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -2311,7 +2311,7 @@
 (* outer syntax *)
 
 val _ =
-  Outer_Syntax.command "record" "define extensible record" Keyword.thy_decl
+  Outer_Syntax.command @{command_spec "record"} "define extensible record"
     (Parse.type_args_constrained -- Parse.binding --
       (@{keyword "="} |-- Scan.option (Parse.typ --| @{keyword "+"}) --
         Scan.repeat1 Parse.const_binding)
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/refute.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -3198,8 +3198,8 @@
 (* 'refute' command *)
 
 val _ =
-  Outer_Syntax.improper_command "refute"
-    "try to find a model that refutes a given subgoal" Keyword.diag
+  Outer_Syntax.improper_command @{command_spec "refute"}
+    "try to find a model that refutes a given subgoal"
     (scan_parms -- Scan.optional Parse.nat 1 >>
       (fn (parms, i) =>
         Toplevel.keep (fn state =>
@@ -3212,8 +3212,8 @@
 (* 'refute_params' command *)
 
 val _ =
-  Outer_Syntax.command "refute_params"
-    "show/store default parameters for the 'refute' command" Keyword.thy_decl
+  Outer_Syntax.command @{command_spec "refute_params"}
+    "show/store default parameters for the 'refute' command"
     (scan_parms >> (fn parms =>
       Toplevel.theory (fn thy =>
         let
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/try0.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -183,13 +183,10 @@
   || Scan.repeat parse_attr
      >> (fn quad => fold merge_attrs quad ([], [], [], []))) x
 
-val parse_try0_command =
-  Scan.optional parse_attrs ([], [], [], []) #>> try0_trans
-
 val _ =
-  Outer_Syntax.improper_command try0N
-      "try a combination of proof methods" Keyword.diag
-      parse_try0_command
+  Outer_Syntax.improper_command @{command_spec "try0"}
+    "try a combination of proof methods"
+    (Scan.optional parse_attrs ([], [], [], []) #>> try0_trans)
 
 fun try_try0 auto =
   do_try0 (if auto then Auto_Try else Try) NONE ([], [], [], [])
diff -r 0c8fb96cce73 -r daf5538144d6 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/typedef.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -300,8 +300,8 @@
 (** outer syntax **)
 
 val _ =
-  Outer_Syntax.local_theory_to_proof "typedef" "HOL type definition (requires non-emptiness proof)"
-    Keyword.thy_goal
+  Outer_Syntax.local_theory_to_proof @{command_spec "typedef"}
+    "HOL type definition (requires non-emptiness proof)"
     (Scan.optional (@{keyword "("} |--
         ((@{keyword "open"} >> K false) -- Scan.option Parse.binding ||
           Parse.binding >> (fn s => (true, SOME s))) --| @{keyword ")"}) (true, NONE) --
diff -r 0c8fb96cce73 -r daf5538144d6 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Provers/classical.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -960,8 +960,7 @@
 (** outer syntax **)
 
 val _ =
-  Outer_Syntax.improper_command "print_claset" "print context of Classical Reasoner"
-    Keyword.diag
+  Outer_Syntax.improper_command @{command_spec "print_claset"} "print context of Classical Reasoner"
     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
       Toplevel.keep (fn state =>
         let val ctxt = Toplevel.context_of state
diff -r 0c8fb96cce73 -r daf5538144d6 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Pure/Isar/isar_syn.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -25,14 +25,14 @@
 (** init and exit **)
 
 val _ =
-  Outer_Syntax.command "theory" "begin theory" (Keyword.tag_theory Keyword.thy_begin)
+  Outer_Syntax.command ("theory", Keyword.tag_theory Keyword.thy_begin) "begin theory"
     (Thy_Header.args >> (fn header =>
       Toplevel.print o
         Toplevel.init_theory
           (fn () => Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) header)));
 
 val _ =
-  Outer_Syntax.command "end" "end (local) theory" (Keyword.tag_theory Keyword.thy_end)
+  Outer_Syntax.command ("end", Keyword.tag_theory Keyword.thy_end) "end (local) theory"
     (Scan.succeed
       (Toplevel.exit o Toplevel.end_local_theory o Toplevel.end_proof (K Proof.end_notepad)));
 
@@ -40,43 +40,65 @@
 
 (** markup commands **)
 
-val _ = Outer_Syntax.markup_command Thy_Output.Markup "header" "theory header" Keyword.diag
-  (Parse.doc_source >> Isar_Cmd.header_markup);
+val _ =
+  Outer_Syntax.markup_command Thy_Output.Markup
+    ("header", Keyword.diag) "theory header"
+    (Parse.doc_source >> Isar_Cmd.header_markup);
 
-val _ = Outer_Syntax.markup_command Thy_Output.Markup "chapter" "chapter heading"
-  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
+val _ =
+  Outer_Syntax.markup_command Thy_Output.Markup
+    ("chapter", Keyword.thy_heading) "chapter heading"
+    (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
 
-val _ = Outer_Syntax.markup_command Thy_Output.Markup "section" "section heading"
-  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
+val _ =
+  Outer_Syntax.markup_command Thy_Output.Markup
+    ("section", Keyword.thy_heading) "section heading"
+    (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
 
-val _ = Outer_Syntax.markup_command Thy_Output.Markup "subsection" "subsection heading"
-  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
+val _ =
+  Outer_Syntax.markup_command Thy_Output.Markup
+    ("subsection", Keyword.thy_heading) "subsection heading"
+    (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
+
+val _ =
+  Outer_Syntax.markup_command Thy_Output.Markup
+    ("subsubsection", Keyword.thy_heading) "subsubsection heading"
+    (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
 
 val _ =
-  Outer_Syntax.markup_command Thy_Output.Markup "subsubsection" "subsubsection heading"
-  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
-
-val _ = Outer_Syntax.markup_command Thy_Output.MarkupEnv "text" "formal comment (theory)"
-  Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
+  Outer_Syntax.markup_command Thy_Output.MarkupEnv
+    ("text", Keyword.thy_decl) "formal comment (theory)"
+    (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
 
-val _ = Outer_Syntax.markup_command Thy_Output.Verbatim "text_raw" "raw document preparation text"
-  Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
+val _ =
+  Outer_Syntax.markup_command Thy_Output.Verbatim
+    ("text_raw", Keyword.thy_decl) "raw document preparation text"
+    (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
 
-val _ = Outer_Syntax.markup_command Thy_Output.Markup "sect" "formal comment (proof)"
-  (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> Isar_Cmd.proof_markup);
+val _ =
+  Outer_Syntax.markup_command Thy_Output.Markup
+    ("sect", Keyword.tag_proof Keyword.prf_heading) "formal comment (proof)"
+    (Parse.doc_source >> Isar_Cmd.proof_markup);
 
-val _ = Outer_Syntax.markup_command Thy_Output.Markup "subsect" "formal comment (proof)"
-  (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> Isar_Cmd.proof_markup);
+val _ =
+  Outer_Syntax.markup_command Thy_Output.Markup
+    ("subsect", Keyword.tag_proof Keyword.prf_heading) "formal comment (proof)"
+    (Parse.doc_source >> Isar_Cmd.proof_markup);
 
-val _ = Outer_Syntax.markup_command Thy_Output.Markup "subsubsect" "formal comment (proof)"
-  (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> Isar_Cmd.proof_markup);
+val _ =
+  Outer_Syntax.markup_command Thy_Output.Markup
+    ("subsubsect", Keyword.tag_proof Keyword.prf_heading) "formal comment (proof)"
+    (Parse.doc_source >> Isar_Cmd.proof_markup);
 
-val _ = Outer_Syntax.markup_command Thy_Output.MarkupEnv "txt" "formal comment (proof)"
-  (Keyword.tag_proof Keyword.prf_decl) (Parse.doc_source >> Isar_Cmd.proof_markup);
+val _ =
+  Outer_Syntax.markup_command Thy_Output.MarkupEnv
+    ("txt", Keyword.tag_proof Keyword.prf_decl) "formal comment (proof)"
+    (Parse.doc_source >> Isar_Cmd.proof_markup);
 
-val _ = Outer_Syntax.markup_command Thy_Output.Verbatim "txt_raw"
-  "raw document preparation text (proof)" (Keyword.tag_proof Keyword.prf_decl)
-  (Parse.doc_source >> Isar_Cmd.proof_markup);
+val _ =
+  Outer_Syntax.markup_command Thy_Output.Verbatim
+    ("txt_raw", Keyword.tag_proof Keyword.prf_decl) "raw document preparation text (proof)"
+    (Parse.doc_source >> Isar_Cmd.proof_markup);
 
 
 
@@ -85,60 +107,60 @@
 (* classes and sorts *)
 
 val _ =
-  Outer_Syntax.command "classes" "declare type classes" Keyword.thy_decl
+  Outer_Syntax.command ("classes", Keyword.thy_decl) "declare type classes"
     (Scan.repeat1 (Parse.binding -- Scan.optional ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |--
         Parse.!!! (Parse.list1 Parse.class)) [])
       >> (Toplevel.theory o fold AxClass.axiomatize_class_cmd));
 
 val _ =
-  Outer_Syntax.command "classrel" "state inclusion of type classes (axiomatic!)" Keyword.thy_decl
+  Outer_Syntax.command ("classrel", Keyword.thy_decl) "state inclusion of type classes (axiomatic!)"
     (Parse.and_list1 (Parse.class -- ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<")
         |-- Parse.!!! Parse.class))
     >> (Toplevel.theory o AxClass.axiomatize_classrel_cmd));
 
 val _ =
-  Outer_Syntax.local_theory "default_sort" "declare default sort for explicit type variables"
-    Keyword.thy_decl
+  Outer_Syntax.local_theory ("default_sort", Keyword.thy_decl)
+    "declare default sort for explicit type variables"
     (Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy));
 
 
 (* types *)
 
 val _ =
-  Outer_Syntax.local_theory "typedecl" "type declaration" Keyword.thy_decl
+  Outer_Syntax.local_theory ("typedecl", Keyword.thy_decl) "type declaration"
     (Parse.type_args -- Parse.binding -- Parse.opt_mixfix
       >> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd));
 
 val _ =
-  Outer_Syntax.local_theory "type_synonym" "declare type abbreviation" Keyword.thy_decl
+  Outer_Syntax.local_theory ("type_synonym", Keyword.thy_decl) "declare type abbreviation"
     (Parse.type_args -- Parse.binding --
       (Parse.$$$ "=" |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'))
       >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs));
 
 val _ =
-  Outer_Syntax.command "nonterminal"
-    "declare syntactic type constructors (grammar nonterminal symbols)" Keyword.thy_decl
+  Outer_Syntax.command ("nonterminal", Keyword.thy_decl)
+    "declare syntactic type constructors (grammar nonterminal symbols)"
     (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global));
 
 val _ =
-  Outer_Syntax.command "arities" "state type arities (axiomatic!)" Keyword.thy_decl
+  Outer_Syntax.command ("arities", Keyword.thy_decl) "state type arities (axiomatic!)"
     (Scan.repeat1 Parse.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity_cmd));
 
 
 (* consts and syntax *)
 
 val _ =
-  Outer_Syntax.command "judgment" "declare object-logic judgment" Keyword.thy_decl
+  Outer_Syntax.command ("judgment", Keyword.thy_decl) "declare object-logic judgment"
     (Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
 
 val _ =
-  Outer_Syntax.command "consts" "declare constants" Keyword.thy_decl
+  Outer_Syntax.command ("consts", Keyword.thy_decl) "declare constants"
     (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts));
 
 val opt_overloaded = Parse.opt_keyword "overloaded";
 
 val _ =
-  Outer_Syntax.command "finalconsts" "declare constants as final" Keyword.thy_decl
+  Outer_Syntax.command ("finalconsts", Keyword.thy_decl) "declare constants as final"
     (opt_overloaded -- Scan.repeat1 Parse.term >> (uncurry (Toplevel.theory oo Theory.add_finals)));
 
 val mode_spec =
@@ -149,11 +171,11 @@
   Scan.optional (Parse.$$$ "(" |-- Parse.!!! (mode_spec --| Parse.$$$ ")")) Syntax.mode_default;
 
 val _ =
-  Outer_Syntax.command "syntax" "declare syntactic constants" Keyword.thy_decl
+  Outer_Syntax.command ("syntax", Keyword.thy_decl) "declare syntactic constants"
     (opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.add_modesyntax));
 
 val _ =
-  Outer_Syntax.command "no_syntax" "delete syntax declarations" Keyword.thy_decl
+  Outer_Syntax.command ("no_syntax", Keyword.thy_decl) "delete syntax declarations"
     (opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.del_modesyntax));
 
 
@@ -174,18 +196,18 @@
     >> (fn (left, (arr, right)) => arr (left, right));
 
 val _ =
-  Outer_Syntax.command "translations" "declare syntax translation rules" Keyword.thy_decl
+  Outer_Syntax.command ("translations", Keyword.thy_decl) "declare syntax translation rules"
     (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations));
 
 val _ =
-  Outer_Syntax.command "no_translations" "remove syntax translation rules" Keyword.thy_decl
+  Outer_Syntax.command ("no_translations", Keyword.thy_decl) "remove syntax translation rules"
     (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations));
 
 
 (* axioms and definitions *)
 
 val _ =
-  Outer_Syntax.command "axioms" "state arbitrary propositions (axiomatic!)" Keyword.thy_decl
+  Outer_Syntax.command ("axioms", Keyword.thy_decl) "state arbitrary propositions (axiomatic!)"
     (Scan.repeat1 Parse_Spec.spec >>
       (fn spec => Toplevel.theory (fn thy =>
         (legacy_feature "Old 'axioms' command -- use 'axiomatization' instead";
@@ -197,7 +219,7 @@
       Parse.$$$ "overloaded" >> K (false, true)) --| Parse.$$$ ")")) (false, false);
 
 val _ =
-  Outer_Syntax.command "defs" "define constants" Keyword.thy_decl
+  Outer_Syntax.command ("defs", Keyword.thy_decl) "define constants"
     (opt_unchecked_overloaded --
       Scan.repeat1 (Parse_Spec.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y)))
       >> (Toplevel.theory o Isar_Cmd.add_defs));
@@ -206,35 +228,35 @@
 (* constant definitions and abbreviations *)
 
 val _ =
-  Outer_Syntax.local_theory' "definition" "constant definition" Keyword.thy_decl
+  Outer_Syntax.local_theory' ("definition", Keyword.thy_decl) "constant definition"
     (Parse_Spec.constdef >> (fn args => #2 oo Specification.definition_cmd args));
 
 val _ =
-  Outer_Syntax.local_theory' "abbreviation" "constant abbreviation" Keyword.thy_decl
+  Outer_Syntax.local_theory' ("abbreviation", Keyword.thy_decl) "constant abbreviation"
     (opt_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
       >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
 
 val _ =
-  Outer_Syntax.local_theory "type_notation" "add concrete syntax for type constructors"
-    Keyword.thy_decl
+  Outer_Syntax.local_theory ("type_notation", Keyword.thy_decl)
+    "add concrete syntax for type constructors"
     (opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
       >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
 
 val _ =
-  Outer_Syntax.local_theory "no_type_notation" "delete concrete syntax for type constructors"
-    Keyword.thy_decl
+  Outer_Syntax.local_theory ("no_type_notation", Keyword.thy_decl)
+    "delete concrete syntax for type constructors"
     (opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
       >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
 
 val _ =
-  Outer_Syntax.local_theory "notation" "add concrete syntax for constants / fixed variables"
-    Keyword.thy_decl
+  Outer_Syntax.local_theory ("notation", Keyword.thy_decl)
+    "add concrete syntax for constants / fixed variables"
     (opt_mode -- Parse.and_list1 (Parse.const -- Parse_Spec.locale_mixfix)
       >> (fn (mode, args) => Specification.notation_cmd true mode args));
 
 val _ =
-  Outer_Syntax.local_theory "no_notation" "delete concrete syntax for constants / fixed variables"
-    Keyword.thy_decl
+  Outer_Syntax.local_theory ("no_notation", Keyword.thy_decl)
+    "delete concrete syntax for constants / fixed variables"
     (opt_mode -- Parse.and_list1 (Parse.const -- Parse_Spec.locale_mixfix)
       >> (fn (mode, args) => Specification.notation_cmd false mode args));
 
@@ -242,7 +264,7 @@
 (* constant specifications *)
 
 val _ =
-  Outer_Syntax.command "axiomatization" "axiomatic constant specification" Keyword.thy_decl
+  Outer_Syntax.command ("axiomatization", Keyword.thy_decl) "axiomatic constant specification"
     (Scan.optional Parse.fixes [] --
       Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 Parse_Spec.specs)) []
       >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));
@@ -255,13 +277,14 @@
     >> (fn (facts, fixes) => #2 oo Specification.theorems_cmd kind facts fixes);
 
 val _ =
-  Outer_Syntax.local_theory' "theorems" "define theorems" Keyword.thy_decl (theorems Thm.theoremK);
+  Outer_Syntax.local_theory' ("theorems", Keyword.thy_decl) "define theorems"
+    (theorems Thm.theoremK);
 
 val _ =
-  Outer_Syntax.local_theory' "lemmas" "define lemmas" Keyword.thy_decl (theorems Thm.lemmaK);
+  Outer_Syntax.local_theory' ("lemmas", Keyword.thy_decl) "define lemmas" (theorems Thm.lemmaK);
 
 val _ =
-  Outer_Syntax.local_theory' "declare" "declare theorems" Keyword.thy_decl
+  Outer_Syntax.local_theory' ("declare", Keyword.thy_decl) "declare theorems"
     (Parse.and_list1 Parse_Spec.xthms1 -- Parse.for_fixes
       >> (fn (facts, fixes) =>
           #2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
@@ -270,7 +293,7 @@
 (* name space entry path *)
 
 fun hide_names name hide what =
-  Outer_Syntax.command name ("hide " ^ what ^ " from name space") Keyword.thy_decl
+  Outer_Syntax.command (name, Keyword.thy_decl) ("hide " ^ what ^ " from name space")
     ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 Parse.xname >>
       (Toplevel.theory o uncurry hide));
 
@@ -283,65 +306,66 @@
 (* use ML text *)
 
 val _ =
-  Outer_Syntax.command "use" "ML text from file" (Keyword.tag_ml Keyword.thy_decl)
+  Outer_Syntax.command ("use", Keyword.tag_ml Keyword.thy_decl) "ML text from file"
     (Parse.path >> (fn path => Toplevel.generic_theory (Thy_Load.exec_ml path)));
 
 val _ =
-  Outer_Syntax.command "ML" "ML text within theory or local theory"
-    (Keyword.tag_ml Keyword.thy_decl)
+  Outer_Syntax.command ("ML", Keyword.tag_ml Keyword.thy_decl)
+    "ML text within theory or local theory"
     (Parse.ML_source >> (fn (txt, pos) =>
       Toplevel.generic_theory
         (ML_Context.exec (fn () => ML_Context.eval_text true pos txt) #>
           Local_Theory.propagate_ml_env)));
 
 val _ =
-  Outer_Syntax.command "ML_prf" "ML text within proof" (Keyword.tag_proof Keyword.prf_decl)
+  Outer_Syntax.command ("ML_prf", Keyword.tag_proof Keyword.prf_decl) "ML text within proof"
     (Parse.ML_source >> (fn (txt, pos) =>
       Toplevel.proof (Proof.map_context (Context.proof_map
         (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> Proof.propagate_ml_env)));
 
 val _ =
-  Outer_Syntax.command "ML_val" "diagnostic ML text" (Keyword.tag_ml Keyword.diag)
+  Outer_Syntax.command ("ML_val", Keyword.tag_ml Keyword.diag) "diagnostic ML text"
     (Parse.ML_source >> Isar_Cmd.ml_diag true);
 
 val _ =
-  Outer_Syntax.command "ML_command" "diagnostic ML text (silent)" (Keyword.tag_ml Keyword.diag)
+  Outer_Syntax.command ("ML_command", Keyword.tag_ml Keyword.diag) "diagnostic ML text (silent)"
     (Parse.ML_source >> (Toplevel.no_timing oo Isar_Cmd.ml_diag false));
 
 val _ =
-  Outer_Syntax.command "setup" "ML theory setup" (Keyword.tag_ml Keyword.thy_decl)
+  Outer_Syntax.command ("setup", Keyword.tag_ml Keyword.thy_decl) "ML theory setup"
     (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.global_setup));
 
 val _ =
-  Outer_Syntax.local_theory "local_setup" "ML local theory setup" (Keyword.tag_ml Keyword.thy_decl)
+  Outer_Syntax.local_theory ("local_setup", Keyword.tag_ml Keyword.thy_decl) "ML local theory setup"
     (Parse.ML_source >> Isar_Cmd.local_setup);
 
 val _ =
-  Outer_Syntax.command "attribute_setup" "define attribute in ML" (Keyword.tag_ml Keyword.thy_decl)
+  Outer_Syntax.command ("attribute_setup", Keyword.tag_ml Keyword.thy_decl) "define attribute in ML"
     (Parse.position Parse.name --
         Parse.!!! (Parse.$$$ "=" |-- Parse.ML_source -- Scan.optional Parse.text "")
       >> (fn (name, (txt, cmt)) => Toplevel.theory (Attrib.attribute_setup name txt cmt)));
 
 val _ =
-  Outer_Syntax.command "method_setup" "define proof method in ML" (Keyword.tag_ml Keyword.thy_decl)
+  Outer_Syntax.command ("method_setup", Keyword.tag_ml Keyword.thy_decl) "define proof method in ML"
     (Parse.position Parse.name --
         Parse.!!! (Parse.$$$ "=" |-- Parse.ML_source -- Scan.optional Parse.text "")
       >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
 
 val _ =
-  Outer_Syntax.local_theory "declaration" "generic ML declaration"
-    (Keyword.tag_ml Keyword.thy_decl)
+  Outer_Syntax.local_theory ("declaration", Keyword.tag_ml Keyword.thy_decl)
+    "generic ML declaration"
     (Parse.opt_keyword "pervasive" -- Parse.ML_source
       >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = false, pervasive = pervasive} txt));
 
 val _ =
-  Outer_Syntax.local_theory "syntax_declaration" "generic ML declaration"
-    (Keyword.tag_ml Keyword.thy_decl)
+  Outer_Syntax.local_theory ("syntax_declaration", Keyword.tag_ml Keyword.thy_decl)
+    "generic ML declaration"
     (Parse.opt_keyword "pervasive" -- Parse.ML_source
       >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = true, pervasive = pervasive} txt));
 
 val _ =
-  Outer_Syntax.local_theory "simproc_setup" "define simproc in ML" (Keyword.tag_ml Keyword.thy_decl)
+  Outer_Syntax.local_theory ("simproc_setup", Keyword.tag_ml Keyword.thy_decl)
+    "define simproc in ML"
     (Parse.position Parse.name --
       (Parse.$$$ "(" |-- Parse.enum1 "|" Parse.term --| Parse.$$$ ")" --| Parse.$$$ "=") --
       Parse.ML_source -- Scan.optional (Parse.$$$ "identifier" |-- Scan.repeat1 Parse.xname) []
@@ -353,35 +377,35 @@
 val trfun = Parse.opt_keyword "advanced" -- Parse.ML_source;
 
 val _ =
-  Outer_Syntax.command "parse_ast_translation" "install parse ast translation functions"
-    (Keyword.tag_ml Keyword.thy_decl)
+  Outer_Syntax.command ("parse_ast_translation", Keyword.tag_ml Keyword.thy_decl)
+    "install parse ast translation functions"
     (trfun >> (Toplevel.theory o Isar_Cmd.parse_ast_translation));
 
 val _ =
-  Outer_Syntax.command "parse_translation" "install parse translation functions"
-    (Keyword.tag_ml Keyword.thy_decl)
+  Outer_Syntax.command ("parse_translation", Keyword.tag_ml Keyword.thy_decl)
+    "install parse translation functions"
     (trfun >> (Toplevel.theory o Isar_Cmd.parse_translation));
 
 val _ =
-  Outer_Syntax.command "print_translation" "install print translation functions"
-    (Keyword.tag_ml Keyword.thy_decl)
+  Outer_Syntax.command ("print_translation", Keyword.tag_ml Keyword.thy_decl)
+    "install print translation functions"
     (trfun >> (Toplevel.theory o Isar_Cmd.print_translation));
 
 val _ =
-  Outer_Syntax.command "typed_print_translation" "install typed print translation functions"
-    (Keyword.tag_ml Keyword.thy_decl)
+  Outer_Syntax.command ("typed_print_translation", Keyword.tag_ml Keyword.thy_decl)
+    "install typed print translation functions"
     (trfun >> (Toplevel.theory o Isar_Cmd.typed_print_translation));
 
 val _ =
-  Outer_Syntax.command "print_ast_translation" "install print ast translation functions"
-    (Keyword.tag_ml Keyword.thy_decl)
+  Outer_Syntax.command ("print_ast_translation", Keyword.tag_ml Keyword.thy_decl)
+    "install print ast translation functions"
     (trfun >> (Toplevel.theory o Isar_Cmd.print_ast_translation));
 
 
 (* oracles *)
 
 val _ =
-  Outer_Syntax.command "oracle" "declare oracle" (Keyword.tag_ml Keyword.thy_decl)
+  Outer_Syntax.command ("oracle", Keyword.tag_ml Keyword.thy_decl) "declare oracle"
     (Parse.position Parse.name -- (Parse.$$$ "=" |-- Parse.ML_source) >>
       (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
 
@@ -389,7 +413,7 @@
 (* local theories *)
 
 val _ =
-  Outer_Syntax.command "context" "enter local theory context" Keyword.thy_decl
+  Outer_Syntax.command ("context", Keyword.thy_decl) "enter local theory context"
     (Parse.position Parse.name --| Parse.begin >> (fn name =>
       Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)));
 
@@ -402,7 +426,7 @@
   Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
 
 val _ =
-  Outer_Syntax.command "locale" "define named proof context" Keyword.thy_decl
+  Outer_Syntax.command ("locale", Keyword.thy_decl) "define named proof context"
     (Parse.binding --
       Scan.optional (Parse.$$$ "=" |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
       >> (fn ((name, (expr, elems)), begin) =>
@@ -415,24 +439,23 @@
       (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
 
 val _ =
-  Outer_Syntax.command "sublocale"
-    "prove sublocale relation between a locale and a locale expression" Keyword.thy_goal
+  Outer_Syntax.command ("sublocale", Keyword.thy_goal)
+    "prove sublocale relation between a locale and a locale expression"
     (Parse.position Parse.xname --| (Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") --
       parse_interpretation_arguments false
       >> (fn (loc, (expr, equations)) =>
           Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd I loc expr equations)));
 
 val _ =
-  Outer_Syntax.command "interpretation"
-    "prove interpretation of locale expression in theory" Keyword.thy_goal
+  Outer_Syntax.command ("interpretation", Keyword.thy_goal)
+    "prove interpretation of locale expression in theory"
     (parse_interpretation_arguments true
       >> (fn (expr, equations) => Toplevel.print o
           Toplevel.theory_to_proof (Expression.interpretation_cmd expr equations)));
 
 val _ =
-  Outer_Syntax.command "interpret"
+  Outer_Syntax.command ("interpret", Keyword.tag_proof Keyword.prf_goal)
     "prove interpretation of locale expression in proof context"
-    (Keyword.tag_proof Keyword.prf_goal)
     (parse_interpretation_arguments true
       >> (fn (expr, equations) => Toplevel.print o
           Toplevel.proof' (Expression.interpret_cmd expr equations)));
@@ -446,24 +469,24 @@
   Scan.repeat1 Parse_Spec.context_element >> pair [];
 
 val _ =
-  Outer_Syntax.command "class" "define type class" Keyword.thy_decl
+  Outer_Syntax.command ("class", Keyword.thy_decl) "define type class"
    (Parse.binding -- Scan.optional (Parse.$$$ "=" |-- class_val) ([], []) -- Parse.opt_begin
     >> (fn ((name, (supclasses, elems)), begin) =>
         (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
           (Class_Declaration.class_cmd I name supclasses elems #> snd)));
 
 val _ =
-  Outer_Syntax.local_theory_to_proof "subclass" "prove a subclass relation" Keyword.thy_goal
+  Outer_Syntax.local_theory_to_proof ("subclass", Keyword.thy_goal) "prove a subclass relation"
     (Parse.class >> Class_Declaration.subclass_cmd I);
 
 val _ =
-  Outer_Syntax.command "instantiation" "instantiate and prove type arity" Keyword.thy_decl
+  Outer_Syntax.command ("instantiation", Keyword.thy_decl) "instantiate and prove type arity"
    (Parse.multi_arity --| Parse.begin
      >> (fn arities => Toplevel.print o
          Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));
 
 val _ =
-  Outer_Syntax.command "instance" "prove type arity or subclass relation" Keyword.thy_goal
+  Outer_Syntax.command ("instance", Keyword.thy_goal) "prove type arity or subclass relation"
   ((Parse.class --
     ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
     Parse.multi_arity >> Class.instance_arity_cmd)
@@ -475,7 +498,7 @@
 (* arbitrary overloading *)
 
 val _ =
-  Outer_Syntax.command "overloading" "overloaded definitions" Keyword.thy_decl
+  Outer_Syntax.command ("overloading", Keyword.thy_decl) "overloaded definitions"
    (Scan.repeat1 (Parse.name --| (Parse.$$$ "\\<equiv>" || Parse.$$$ "==") -- Parse.term --
       Scan.optional (Parse.$$$ "(" |-- (Parse.$$$ "unchecked" >> K false) --| Parse.$$$ ")") true
       >> Parse.triple1) --| Parse.begin
@@ -486,7 +509,8 @@
 (* code generation *)
 
 val _ =
-  Outer_Syntax.command "code_datatype" "define set of code datatype constructors" Keyword.thy_decl
+  Outer_Syntax.command ("code_datatype", Keyword.thy_decl)
+    "define set of code datatype constructors"
     (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.add_datatype_cmd));
 
 
@@ -497,9 +521,9 @@
 
 fun gen_theorem schematic kind =
   Outer_Syntax.local_theory_to_proof'
-    (if schematic then "schematic_" ^ kind else kind)
+    (if schematic then ("schematic_" ^ kind, Keyword.thy_schematic_goal)
+     else (kind, Keyword.thy_goal))
     ("state " ^ (if schematic then "schematic " ^ kind else kind))
-    (if schematic then Keyword.thy_schematic_goal else Keyword.thy_goal)
     (Scan.optional (Parse_Spec.opt_thm_name ":" --|
       Scan.ahead (Parse_Spec.locale_keyword || Parse_Spec.statement_keyword)) Attrib.empty_binding --
       Parse_Spec.general_statement >> (fn (a, (elems, concl)) =>
@@ -514,28 +538,25 @@
 val _ = gen_theorem true Thm.corollaryK;
 
 val _ =
-  Outer_Syntax.local_theory_to_proof "notepad"
-    "Isar proof state as formal notepad, without any result" Keyword.thy_decl
+  Outer_Syntax.local_theory_to_proof ("notepad", Keyword.thy_decl)
+    "Isar proof state as formal notepad, without any result"
     (Parse.begin >> K Proof.begin_notepad);
 
 val _ =
-  Outer_Syntax.command "have" "state local goal"
-    (Keyword.tag_proof Keyword.prf_goal)
+  Outer_Syntax.command ("have", Keyword.tag_proof Keyword.prf_goal) "state local goal"
     (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.have));
 
 val _ =
-  Outer_Syntax.command "hence" "abbreviates \"then have\""
-    (Keyword.tag_proof Keyword.prf_goal)
+  Outer_Syntax.command ("hence", Keyword.tag_proof Keyword.prf_goal) "abbreviates \"then have\""
     (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.hence));
 
 val _ =
-  Outer_Syntax.command "show" "state local goal, solving current obligation"
-    (Keyword.tag_proof Keyword.prf_asm_goal)
+  Outer_Syntax.command ("show", Keyword.tag_proof Keyword.prf_asm_goal)
+    "state local goal, solving current obligation"
     (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.show));
 
 val _ =
-  Outer_Syntax.command "thus" "abbreviates \"then show\""
-    (Keyword.tag_proof Keyword.prf_asm_goal)
+  Outer_Syntax.command ("thus", Keyword.tag_proof Keyword.prf_asm_goal) "abbreviates \"then show\""
     (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.thus));
 
 
@@ -544,56 +565,51 @@
 val facts = Parse.and_list1 Parse_Spec.xthms1;
 
 val _ =
-  Outer_Syntax.command "then" "forward chaining"
-    (Keyword.tag_proof Keyword.prf_chain)
+  Outer_Syntax.command ("then", Keyword.tag_proof Keyword.prf_chain) "forward chaining"
     (Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain));
 
 val _ =
-  Outer_Syntax.command "from" "forward chaining from given facts"
-    (Keyword.tag_proof Keyword.prf_chain)
+  Outer_Syntax.command ("from", Keyword.tag_proof Keyword.prf_chain)
+    "forward chaining from given facts"
     (facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss_cmd)));
 
 val _ =
-  Outer_Syntax.command "with" "forward chaining from given and current facts"
-    (Keyword.tag_proof Keyword.prf_chain)
+  Outer_Syntax.command ("with", Keyword.tag_proof Keyword.prf_chain)
+    "forward chaining from given and current facts"
     (facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss_cmd)));
 
 val _ =
-  Outer_Syntax.command "note" "define facts"
-    (Keyword.tag_proof Keyword.prf_decl)
+  Outer_Syntax.command ("note", Keyword.tag_proof Keyword.prf_decl) "define facts"
     (Parse_Spec.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss_cmd)));
 
 val _ =
-  Outer_Syntax.command "using" "augment goal facts"
-    (Keyword.tag_proof Keyword.prf_decl)
+  Outer_Syntax.command ("using", Keyword.tag_proof Keyword.prf_decl) "augment goal facts"
     (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using_cmd)));
 
 val _ =
-  Outer_Syntax.command "unfolding" "unfold definitions in goal and facts"
-    (Keyword.tag_proof Keyword.prf_decl)
+  Outer_Syntax.command ("unfolding", Keyword.tag_proof Keyword.prf_decl)
+    "unfold definitions in goal and facts"
     (facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding_cmd)));
 
 
 (* proof context *)
 
 val _ =
-  Outer_Syntax.command "fix" "fix local variables (Skolem constants)"
-    (Keyword.tag_proof Keyword.prf_asm)
+  Outer_Syntax.command ("fix", Keyword.tag_proof Keyword.prf_asm)
+    "fix local variables (Skolem constants)"
     (Parse.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix_cmd)));
 
 val _ =
-  Outer_Syntax.command "assume" "assume propositions"
-    (Keyword.tag_proof Keyword.prf_asm)
+  Outer_Syntax.command ("assume", Keyword.tag_proof Keyword.prf_asm) "assume propositions"
     (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume_cmd)));
 
 val _ =
-  Outer_Syntax.command "presume" "assume propositions, to be established later"
-    (Keyword.tag_proof Keyword.prf_asm)
+  Outer_Syntax.command ("presume", Keyword.tag_proof Keyword.prf_asm)
+    "assume propositions, to be established later"
     (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd)));
 
 val _ =
-  Outer_Syntax.command "def" "local definition"
-    (Keyword.tag_proof Keyword.prf_asm)
+  Outer_Syntax.command ("def", Keyword.tag_proof Keyword.prf_asm) "local definition"
     (Parse.and_list1
       (Parse_Spec.opt_thm_name ":" --
         ((Parse.binding -- Parse.opt_mixfix) --
@@ -601,25 +617,24 @@
     >> (Toplevel.print oo (Toplevel.proof o Proof.def_cmd)));
 
 val _ =
-  Outer_Syntax.command "obtain" "generalized existence"
-    (Keyword.tag_proof Keyword.prf_asm_goal)
+  Outer_Syntax.command ("obtain", Keyword.tag_proof Keyword.prf_asm_goal)
+    "generalized elimination"
     (Parse.parname -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement
       >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain_cmd x y z)));
 
 val _ =
-  Outer_Syntax.command "guess" "wild guessing (unstructured)"
-    (Keyword.tag_proof Keyword.prf_asm_goal)
+  Outer_Syntax.command ("guess", Keyword.tag_proof Keyword.prf_asm_goal)
+    "wild guessing (unstructured)"
     (Scan.optional Parse.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess_cmd)));
 
 val _ =
-  Outer_Syntax.command "let" "bind text variables"
-    (Keyword.tag_proof Keyword.prf_decl)
+  Outer_Syntax.command ("let", Keyword.tag_proof Keyword.prf_decl) "bind text variables"
     (Parse.and_list1 (Parse.and_list1 Parse.term -- (Parse.$$$ "=" |-- Parse.term))
       >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind_cmd)));
 
 val _ =
-  Outer_Syntax.command "write" "add concrete syntax for constants / fixed variables"
-    (Keyword.tag_proof Keyword.prf_decl)
+  Outer_Syntax.command ("write", Keyword.tag_proof Keyword.prf_decl)
+    "add concrete syntax for constants / fixed variables"
     (opt_mode -- Parse.and_list1 (Parse.const -- Parse_Spec.locale_mixfix)
     >> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args)));
 
@@ -629,92 +644,81 @@
     Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> Parse.triple1;
 
 val _ =
-  Outer_Syntax.command "case" "invoke local context"
-    (Keyword.tag_proof Keyword.prf_asm)
+  Outer_Syntax.command ("case", Keyword.tag_proof Keyword.prf_asm) "invoke local context"
     (case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case_cmd)));
 
 
 (* proof structure *)
 
 val _ =
-  Outer_Syntax.command "{" "begin explicit proof block"
-    (Keyword.tag_proof Keyword.prf_open)
+  Outer_Syntax.command ("{", Keyword.tag_proof Keyword.prf_open) "begin explicit proof block"
     (Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block));
 
 val _ =
-  Outer_Syntax.command "}" "end explicit proof block"
-    (Keyword.tag_proof Keyword.prf_close)
+  Outer_Syntax.command ("}", Keyword.tag_proof Keyword.prf_close) "end explicit proof block"
     (Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block));
 
 val _ =
-  Outer_Syntax.command "next" "enter next proof block"
-    (Keyword.tag_proof Keyword.prf_block)
+  Outer_Syntax.command ("next", Keyword.tag_proof Keyword.prf_block) "enter next proof block"
     (Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block));
 
 
 (* end proof *)
 
 val _ =
-  Outer_Syntax.command "qed" "conclude (sub-)proof"
-    (Keyword.tag_proof Keyword.qed_block)
+  Outer_Syntax.command ("qed", Keyword.tag_proof Keyword.qed_block) "conclude (sub-)proof"
     (Scan.option Method.parse >> Isar_Cmd.qed);
 
 val _ =
-  Outer_Syntax.command "by" "terminal backward proof"
-    (Keyword.tag_proof Keyword.qed)
+  Outer_Syntax.command ("by", Keyword.tag_proof Keyword.qed) "terminal backward proof"
     (Method.parse -- Scan.option Method.parse >> Isar_Cmd.terminal_proof);
 
 val _ =
-  Outer_Syntax.command ".." "default proof"
-    (Keyword.tag_proof Keyword.qed)
+  Outer_Syntax.command ("..", Keyword.tag_proof Keyword.qed) "default proof"
     (Scan.succeed Isar_Cmd.default_proof);
 
 val _ =
-  Outer_Syntax.command "." "immediate proof"
-    (Keyword.tag_proof Keyword.qed)
+  Outer_Syntax.command (".", Keyword.tag_proof Keyword.qed) "immediate proof"
     (Scan.succeed Isar_Cmd.immediate_proof);
 
 val _ =
-  Outer_Syntax.command "done" "done proof"
-    (Keyword.tag_proof Keyword.qed)
+  Outer_Syntax.command ("done", Keyword.tag_proof Keyword.qed) "done proof"
     (Scan.succeed Isar_Cmd.done_proof);
 
 val _ =
-  Outer_Syntax.command "sorry" "skip proof (quick-and-dirty mode only!)"
-    (Keyword.tag_proof Keyword.qed)
+  Outer_Syntax.command ("sorry", Keyword.tag_proof Keyword.qed)
+    "skip proof (quick-and-dirty mode only!)"
     (Scan.succeed Isar_Cmd.skip_proof);
 
 val _ =
-  Outer_Syntax.command "oops" "forget proof"
-    (Keyword.tag_proof Keyword.qed_global)
+  Outer_Syntax.command ("oops", Keyword.tag_proof Keyword.qed_global) "forget proof"
     (Scan.succeed Toplevel.forget_proof);
 
 
 (* proof steps *)
 
 val _ =
-  Outer_Syntax.command "defer" "shuffle internal proof state"
-    (Keyword.tag_proof Keyword.prf_script)
+  Outer_Syntax.command ("defer", Keyword.tag_proof Keyword.prf_script)
+    "shuffle internal proof state"
     (Scan.option Parse.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.defer)));
 
 val _ =
-  Outer_Syntax.command "prefer" "shuffle internal proof state"
-    (Keyword.tag_proof Keyword.prf_script)
+  Outer_Syntax.command ("prefer", Keyword.tag_proof Keyword.prf_script)
+    "shuffle internal proof state"
     (Parse.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.prefer)));
 
 val _ =
-  Outer_Syntax.command "apply" "initial refinement step (unstructured)"
-    (Keyword.tag_proof Keyword.prf_script)
+  Outer_Syntax.command ("apply", Keyword.tag_proof Keyword.prf_script)
+    "initial refinement step (unstructured)"
     (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply)));
 
 val _ =
-  Outer_Syntax.command "apply_end" "terminal refinement (unstructured)"
-    (Keyword.tag_proof Keyword.prf_script)
+  Outer_Syntax.command ("apply_end", Keyword.tag_proof Keyword.prf_script)
+    "terminal refinement (unstructured)"
     (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end)));
 
 val _ =
-  Outer_Syntax.command "proof" "backward proof"
-    (Keyword.tag_proof Keyword.prf_block)
+  Outer_Syntax.command ("proof", Keyword.tag_proof Keyword.prf_block) "backward proof"
     (Scan.option Method.parse >> (fn m => Toplevel.print o
       Toplevel.actual_proof (Proof_Node.applys (Proof.proof m)) o
       Toplevel.skip_proof (fn i => i + 1)));
@@ -726,31 +730,31 @@
   Scan.option (Parse.$$$ "(" |-- Parse.!!! ((Parse_Spec.xthms1 --| Parse.$$$ ")")));
 
 val _ =
-  Outer_Syntax.command "also" "combine calculation and current facts"
-    (Keyword.tag_proof Keyword.prf_decl)
+  Outer_Syntax.command ("also", Keyword.tag_proof Keyword.prf_decl)
+    "combine calculation and current facts"
     (calc_args >> (Toplevel.proofs' o Calculation.also_cmd));
 
 val _ =
-  Outer_Syntax.command "finally" "combine calculation and current facts, exhibit result"
-    (Keyword.tag_proof Keyword.prf_chain)
+  Outer_Syntax.command ("finally", Keyword.tag_proof Keyword.prf_chain)
+    "combine calculation and current facts, exhibit result"
     (calc_args >> (Toplevel.proofs' o Calculation.finally_cmd));
 
 val _ =
-  Outer_Syntax.command "moreover" "augment calculation by current facts"
-    (Keyword.tag_proof Keyword.prf_decl)
+  Outer_Syntax.command ("moreover", Keyword.tag_proof Keyword.prf_decl)
+    "augment calculation by current facts"
     (Scan.succeed (Toplevel.proof' Calculation.moreover));
 
 val _ =
-  Outer_Syntax.command "ultimately" "augment calculation by current facts, exhibit result"
-    (Keyword.tag_proof Keyword.prf_chain)
+  Outer_Syntax.command ("ultimately", Keyword.tag_proof Keyword.prf_chain)
+    "augment calculation by current facts, exhibit result"
     (Scan.succeed (Toplevel.proof' Calculation.ultimately));
 
 
 (* proof navigation *)
 
 val _ =
-  Outer_Syntax.command "back" "backtracking of proof command"
-    (Keyword.tag_proof Keyword.prf_script)
+  Outer_Syntax.command ("back", Keyword.tag_proof Keyword.prf_script)
+    "backtracking of proof command"
     (Scan.succeed (Toplevel.print o Toplevel.actual_proof Proof_Node.back o Toplevel.skip_proof I));
 
 
@@ -762,7 +766,7 @@
       (Position.of_properties (Position.default_properties pos props), str));
 
 val _ =
-  Outer_Syntax.improper_command "Isabelle.command" "nested Isabelle command" Keyword.control
+  Outer_Syntax.improper_command ("Isabelle.command", Keyword.control) "nested Isabelle command"
     (props_text :|-- (fn (pos, str) =>
       (case Outer_Syntax.parse pos str of
         [tr] => Scan.succeed (K tr)
@@ -779,152 +783,161 @@
 val opt_bang = Scan.optional (Parse.$$$ "!" >> K true) false;
 
 val _ =
-  Outer_Syntax.improper_command "pretty_setmargin" "change default margin for pretty printing"
-    Keyword.diag (Parse.nat >>
+  Outer_Syntax.improper_command ("pretty_setmargin", Keyword.diag)
+    "change default margin for pretty printing"
+    (Parse.nat >>
       (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Pretty.margin_default := n)));
 
 val _ =
-  Outer_Syntax.improper_command "help" "print outer syntax commands" Keyword.diag
+  Outer_Syntax.improper_command ("help", Keyword.diag) "print outer syntax commands"
     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Outer_Syntax.print_outer_syntax));
 
 val _ =
-  Outer_Syntax.improper_command "print_commands" "print outer syntax commands" Keyword.diag
+  Outer_Syntax.improper_command ("print_commands", Keyword.diag) "print outer syntax commands"
     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Outer_Syntax.print_outer_syntax));
 
 val _ =
-  Outer_Syntax.improper_command "print_configs" "print configuration options" Keyword.diag
+  Outer_Syntax.improper_command ("print_configs", Keyword.diag) "print configuration options"
     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_configs));
 
 val _ =
-  Outer_Syntax.improper_command "print_context" "print theory context name" Keyword.diag
+  Outer_Syntax.improper_command ("print_context", Keyword.diag) "print theory context name"
     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_context));
 
 val _ =
-  Outer_Syntax.improper_command "print_theory" "print logical theory contents (verbose!)"
-    Keyword.diag (opt_bang >> (Toplevel.no_timing oo Isar_Cmd.print_theory));
+  Outer_Syntax.improper_command ("print_theory", Keyword.diag)
+    "print logical theory contents (verbose!)"
+    (opt_bang >> (Toplevel.no_timing oo Isar_Cmd.print_theory));
 
 val _ =
-  Outer_Syntax.improper_command "print_syntax" "print inner syntax of context (verbose!)"
-    Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_syntax));
+  Outer_Syntax.improper_command ("print_syntax", Keyword.diag)
+    "print inner syntax of context (verbose!)"
+    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_syntax));
 
 val _ =
-  Outer_Syntax.improper_command "print_abbrevs" "print constant abbreviation of context"
-    Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_abbrevs));
+  Outer_Syntax.improper_command ("print_abbrevs", Keyword.diag)
+    "print constant abbreviation of context"
+    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_abbrevs));
 
 val _ =
-  Outer_Syntax.improper_command "print_theorems"
-      "print theorems of local theory or proof context" Keyword.diag
+  Outer_Syntax.improper_command ("print_theorems", Keyword.diag)
+    "print theorems of local theory or proof context"
     (opt_bang >> (Toplevel.no_timing oo Isar_Cmd.print_theorems));
 
 val _ =
-  Outer_Syntax.improper_command "print_locales" "print locales of this theory" Keyword.diag
+  Outer_Syntax.improper_command ("print_locales", Keyword.diag)
+    "print locales of this theory"
     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_locales));
 
 val _ =
-  Outer_Syntax.improper_command "print_classes" "print classes of this theory" Keyword.diag
+  Outer_Syntax.improper_command ("print_classes", Keyword.diag) "print classes of this theory"
     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
       Toplevel.keep (Class.print_classes o Toplevel.context_of)));
 
 val _ =
-  Outer_Syntax.improper_command "print_locale" "print locale of this theory" Keyword.diag
+  Outer_Syntax.improper_command ("print_locale", Keyword.diag) "print locale of this theory"
     (opt_bang -- Parse.position Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_locale));
 
 val _ =
-  Outer_Syntax.improper_command "print_interps"
-    "print interpretations of locale for this theory or proof context" Keyword.diag
+  Outer_Syntax.improper_command ("print_interps", Keyword.diag)
+    "print interpretations of locale for this theory or proof context"
     (Parse.position Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_registrations));
 
 val _ =
-  Outer_Syntax.improper_command "print_dependencies"
-    "print dependencies of locale expression" Keyword.diag
+  Outer_Syntax.improper_command ("print_dependencies", Keyword.diag)
+    "print dependencies of locale expression"
     (opt_bang -- Parse_Spec.locale_expression true >>
       (Toplevel.no_timing oo Isar_Cmd.print_dependencies));
 
 val _ =
-  Outer_Syntax.improper_command "print_attributes" "print attributes of this theory" Keyword.diag
+  Outer_Syntax.improper_command ("print_attributes", Keyword.diag)
+    "print attributes of this theory"
     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_attributes));
 
 val _ =
-  Outer_Syntax.improper_command "print_simpset" "print context of Simplifier" Keyword.diag
+  Outer_Syntax.improper_command ("print_simpset", Keyword.diag)
+    "print context of Simplifier"
     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_simpset));
 
 val _ =
-  Outer_Syntax.improper_command "print_rules" "print intro/elim rules" Keyword.diag
+  Outer_Syntax.improper_command ("print_rules", Keyword.diag) "print intro/elim rules"
     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_rules));
 
 val _ =
-  Outer_Syntax.improper_command "print_trans_rules" "print transitivity rules" Keyword.diag
+  Outer_Syntax.improper_command ("print_trans_rules", Keyword.diag) "print transitivity rules"
     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_trans_rules));
 
 val _ =
-  Outer_Syntax.improper_command "print_methods" "print methods of this theory" Keyword.diag
+  Outer_Syntax.improper_command ("print_methods", Keyword.diag) "print methods of this theory"
     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_methods));
 
 val _ =
-  Outer_Syntax.improper_command "print_antiquotations" "print antiquotations (global)" Keyword.diag
+  Outer_Syntax.improper_command ("print_antiquotations", Keyword.diag)
+    "print antiquotations (global)"
     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_antiquotations));
 
 val _ =
-  Outer_Syntax.improper_command "thy_deps" "visualize theory dependencies"
-    Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.thy_deps));
+  Outer_Syntax.improper_command ("thy_deps", Keyword.diag) "visualize theory dependencies"
+    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.thy_deps));
 
 val _ =
-  Outer_Syntax.improper_command "class_deps" "visualize class dependencies"
-    Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.class_deps));
+  Outer_Syntax.improper_command ("class_deps", Keyword.diag) "visualize class dependencies"
+    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.class_deps));
 
 val _ =
-  Outer_Syntax.improper_command "thm_deps" "visualize theorem dependencies"
-    Keyword.diag (Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.thm_deps));
+  Outer_Syntax.improper_command ("thm_deps", Keyword.diag) "visualize theorem dependencies"
+    (Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.thm_deps));
 
 val _ =
-  Outer_Syntax.improper_command "print_binds" "print term bindings of proof context" Keyword.diag
+  Outer_Syntax.improper_command ("print_binds", Keyword.diag) "print term bindings of proof context"
     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_binds));
 
 val _ =
-  Outer_Syntax.improper_command "print_facts" "print facts of proof context" Keyword.diag
+  Outer_Syntax.improper_command ("print_facts", Keyword.diag) "print facts of proof context"
     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_facts));
 
 val _ =
-  Outer_Syntax.improper_command "print_cases" "print cases of proof context" Keyword.diag
+  Outer_Syntax.improper_command ("print_cases", Keyword.diag) "print cases of proof context"
     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_cases));
 
 val _ =
-  Outer_Syntax.improper_command "print_statement" "print theorems as long statements" Keyword.diag
+  Outer_Syntax.improper_command ("print_statement", Keyword.diag)
+    "print theorems as long statements"
     (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_stmts));
 
 val _ =
-  Outer_Syntax.improper_command "thm" "print theorems" Keyword.diag
+  Outer_Syntax.improper_command ("thm", Keyword.diag) "print theorems"
     (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_thms));
 
 val _ =
-  Outer_Syntax.improper_command "prf" "print proof terms of theorems" Keyword.diag
+  Outer_Syntax.improper_command ("prf", Keyword.diag) "print proof terms of theorems"
     (opt_modes -- Scan.option Parse_Spec.xthms1
       >> (Toplevel.no_timing oo Isar_Cmd.print_prfs false));
 
 val _ =
-  Outer_Syntax.improper_command "full_prf" "print full proof terms of theorems" Keyword.diag
+  Outer_Syntax.improper_command ("full_prf", Keyword.diag) "print full proof terms of theorems"
     (opt_modes -- Scan.option Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_prfs true));
 
 val _ =
-  Outer_Syntax.improper_command "prop" "read and print proposition" Keyword.diag
+  Outer_Syntax.improper_command ("prop", Keyword.diag) "read and print proposition"
     (opt_modes -- Parse.term >> (Toplevel.no_timing oo Isar_Cmd.print_prop));
 
 val _ =
-  Outer_Syntax.improper_command "term" "read and print term" Keyword.diag
+  Outer_Syntax.improper_command ("term", Keyword.diag) "read and print term"
     (opt_modes -- Parse.term >> (Toplevel.no_timing oo Isar_Cmd.print_term));
 
 val _ =
-  Outer_Syntax.improper_command "typ" "read and print type" Keyword.diag
+  Outer_Syntax.improper_command ("typ", Keyword.diag) "read and print type"
     (opt_modes -- Parse.typ >> (Toplevel.no_timing oo Isar_Cmd.print_type));
 
 val _ =
-  Outer_Syntax.improper_command "print_codesetup" "print code generator setup" Keyword.diag
+  Outer_Syntax.improper_command ("print_codesetup", Keyword.diag) "print code generator setup"
     (Scan.succeed
       (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
         (Code.print_codesetup o Toplevel.theory_of)));
 
 val _ =
-  Outer_Syntax.improper_command "unused_thms" "find unused theorems" Keyword.diag
+  Outer_Syntax.improper_command ("unused_thms", Keyword.diag) "find unused theorems"
     (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
        Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >>
          (Toplevel.no_timing oo Isar_Cmd.unused_thms));
@@ -934,39 +947,42 @@
 (** system commands (for interactive mode only) **)
 
 val _ =
-  Outer_Syntax.improper_command "cd" "change current working directory" Keyword.control
+  Outer_Syntax.improper_command ("cd", Keyword.control) "change current working directory"
     (Parse.path >> (fn path => Toplevel.no_timing o Toplevel.imperative (fn () => File.cd path)));
 
 val _ =
-  Outer_Syntax.improper_command "pwd" "print current working directory" Keyword.diag
+  Outer_Syntax.improper_command ("pwd", Keyword.diag) "print current working directory"
     (Scan.succeed (Toplevel.no_timing o
       Toplevel.imperative (fn () => writeln (Path.print (File.pwd ())))));
 
 val _ =
-  Outer_Syntax.improper_command "use_thy" "use theory file" Keyword.control
+  Outer_Syntax.improper_command ("use_thy", Keyword.control) "use theory file"
     (Parse.name >> (fn name =>
       Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.use_thy name)));
 
 val _ =
-  Outer_Syntax.improper_command "remove_thy" "remove theory from loader database" Keyword.control
+  Outer_Syntax.improper_command ("remove_thy", Keyword.control) "remove theory from loader database"
     (Parse.name >> (fn name =>
       Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.remove_thy name)));
 
 val _ =
-  Outer_Syntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"
-    Keyword.control (Parse.name >> (fn name =>
+  Outer_Syntax.improper_command ("kill_thy", Keyword.control)
+    "kill theory -- try to remove from loader database"
+    (Parse.name >> (fn name =>
       Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.kill_thy name)));
 
 val _ =
-  Outer_Syntax.improper_command "display_drafts" "display raw source files with symbols"
-    Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.display_drafts));
+  Outer_Syntax.improper_command ("display_drafts", Keyword.diag)
+    "display raw source files with symbols"
+    (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.display_drafts));
 
 val _ =
-  Outer_Syntax.improper_command "print_drafts" "print raw source files with symbols"
-    Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.print_drafts));
+  Outer_Syntax.improper_command ("print_drafts", Keyword.diag)
+    "print raw source files with symbols"
+    (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.print_drafts));
 
 val _ =  (* FIXME tty only *)
-  Outer_Syntax.improper_command "pr" "print current proof state (if present)" Keyword.diag
+  Outer_Syntax.improper_command ("pr", Keyword.diag) "print current proof state (if present)"
     (opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) =>
       Toplevel.no_timing o Toplevel.keep (fn state =>
        (case limit of NONE => () | SOME n => Goal_Display.goals_limit_default := n;
@@ -974,23 +990,26 @@
         Print_Mode.with_modes modes (Toplevel.print_state true) state))));
 
 val _ =
-  Outer_Syntax.improper_command "disable_pr" "disable printing of toplevel state" Keyword.control
+  Outer_Syntax.improper_command ("disable_pr", Keyword.control)
+    "disable printing of toplevel state"
     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Toplevel.quiet := true)));
 
 val _ =
-  Outer_Syntax.improper_command "enable_pr" "enable printing of toplevel state" Keyword.control
+  Outer_Syntax.improper_command ("enable_pr", Keyword.control)
+    "enable printing of toplevel state"
     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Toplevel.quiet := false)));
 
 val _ =
-  Outer_Syntax.improper_command "commit" "commit current session to ML database" Keyword.control
+  Outer_Syntax.improper_command ("commit", Keyword.control)
+    "commit current session to ML database"
     (Parse.opt_unit >> K (Toplevel.no_timing o Toplevel.imperative Secure.commit));
 
 val _ =
-  Outer_Syntax.improper_command "quit" "quit Isabelle" Keyword.control
+  Outer_Syntax.improper_command ("quit", Keyword.control) "quit Isabelle"
     (Parse.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative quit)));
 
 val _ =
-  Outer_Syntax.improper_command "exit" "exit Isar loop" Keyword.control
+  Outer_Syntax.improper_command ("exit", Keyword.control) "exit Isar loop"
     (Scan.succeed
       (Toplevel.no_timing o Toplevel.keep (fn state =>
         (Context.set_thread_data (try Toplevel.generic_theory_of state);
diff -r 0c8fb96cce73 -r daf5538144d6 src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Pure/Isar/keyword.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -37,7 +37,9 @@
   val tag_theory: T -> T
   val tag_proof: T -> T
   val tag_ml: T -> T
-  val make: string * string list -> T
+  type spec = string * string list
+  val spec: spec -> T
+  val command_spec: string * spec -> string * T
   val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
   val is_keyword: string -> bool
   val command_keyword: string -> T option
@@ -65,7 +67,7 @@
 
 (** keyword classification **)
 
-datatype T = Keyword of string * string list;
+datatype T = Keyword of string * string list;  (*kind, tags (in canonical reverse order)*)
 
 fun kind s = Keyword (s, []);
 fun kind_of (Keyword (s, _)) = s;
@@ -141,11 +143,15 @@
    ("prf_asm_goal",       prf_asm_goal),
    ("prf_script",         prf_script)];
 
-fun make (kind, tags) =
+type spec = string * string list;
+
+fun spec (kind, tags) =
   (case Symtab.lookup name_table kind of
     SOME k => k |> fold tag tags
   | NONE => error ("Unknown outer syntax keyword kind " ^ quote kind));
 
+fun command_spec (name, s) = (name, spec s);
+
 
 
 (** global keyword tables **)
diff -r 0c8fb96cce73 -r daf5538144d6 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -12,21 +12,20 @@
   type outer_syntax
   val is_markup: outer_syntax -> Thy_Output.markup -> string -> bool
   val get_syntax: unit -> (Scan.lexicon * Scan.lexicon) * outer_syntax
-  val command: string -> string -> Keyword.T ->
-    (Toplevel.transition -> Toplevel.transition) parser -> unit
-  val markup_command: Thy_Output.markup -> string -> string -> Keyword.T ->
+  type command_spec = string * Keyword.T
+  val command: command_spec -> string ->
     (Toplevel.transition -> Toplevel.transition) parser -> unit
-  val improper_command: string -> string -> Keyword.T ->
+  val markup_command: Thy_Output.markup -> command_spec -> string ->
     (Toplevel.transition -> Toplevel.transition) parser -> unit
-  val internal_command: string ->
+  val improper_command: command_spec -> string ->
     (Toplevel.transition -> Toplevel.transition) parser -> unit
-  val local_theory': string -> string -> Keyword.T ->
+  val local_theory': command_spec -> string ->
     (bool -> local_theory -> local_theory) parser -> unit
-  val local_theory: string -> string -> Keyword.T ->
+  val local_theory: command_spec -> string ->
     (local_theory -> local_theory) parser -> unit
-  val local_theory_to_proof': string -> string -> Keyword.T ->
+  val local_theory_to_proof': command_spec -> string ->
     (bool -> local_theory -> Proof.state) parser -> unit
-  val local_theory_to_proof: string -> string -> Keyword.T ->
+  val local_theory_to_proof: command_spec -> string ->
     (local_theory -> Proof.state) parser -> unit
   val print_outer_syntax: unit -> unit
   val scan: Position.T -> string -> Token.T list
@@ -117,21 +116,24 @@
 
 (** global outer syntax **)
 
+type command_spec = string * Keyword.T;
+
 local
 
 (*synchronized wrt. Keywords*)
 val global_outer_syntax = Unsynchronized.ref empty_outer_syntax;
 
-fun add_command name kind cmd = CRITICAL (fn () =>
+fun add_command (name, kind) cmd = CRITICAL (fn () =>
   let
     val thy = ML_Context.the_global_context ();
     val _ =
       (case try (Thy_Header.the_keyword thy) name of
-        SOME k =>
-          if k = SOME kind then ()
+        SOME spec =>
+          if Option.map Keyword.spec spec = SOME kind then ()
           else error ("Inconsistent outer syntax keyword declaration " ^ quote name)
       | NONE =>
-          if Context.theory_name thy = Context.PureN then Keyword.define (name, SOME kind)
+          if Context.theory_name thy = Context.PureN
+          then Keyword.define (name, SOME kind)
           else error ("Undeclared outer syntax command " ^ quote name));
   in
     Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
@@ -146,25 +148,22 @@
 
 fun lookup_commands_dynamic () = lookup_commands (! global_outer_syntax);
 
-fun command name comment kind parse =
-  add_command name kind (make_command comment NONE false parse);
-
-fun markup_command markup name comment kind parse =
-  add_command name kind (make_command comment (SOME markup) false parse);
+fun command command_spec comment parse =
+  add_command command_spec (make_command comment NONE false parse);
 
-fun improper_command name comment kind parse =
-  add_command name kind (make_command comment NONE true parse);
+fun markup_command markup command_spec comment parse =
+  add_command command_spec (make_command comment (SOME markup) false parse);
 
-fun internal_command name parse =
-  command name "(internal)" Keyword.control (parse >> (fn tr => Toplevel.no_timing o tr));
+fun improper_command command_spec comment parse =
+  add_command command_spec (make_command comment NONE true parse);
 
 end;
 
 
 (* local_theory commands *)
 
-fun local_theory_command do_print trans name comment kind parse =
-  command name comment kind (Parse.opt_target -- parse
+fun local_theory_command do_print trans command_spec comment parse =
+  command command_spec comment (Parse.opt_target -- parse
     >> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f));
 
 val local_theory' = local_theory_command false Toplevel.local_theory';
diff -r 0c8fb96cce73 -r daf5538144d6 src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Pure/ML/ml_antiquote.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -66,8 +66,7 @@
   inline (Binding.name "make_string") (Scan.succeed ml_make_string) #>
 
   value (Binding.name "binding")
-    (Scan.lift (Parse.position Args.name)
-      >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name))) #>
+    (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #>
 
   value (Binding.name "theory")
     (Scan.lift Args.name >> (fn name =>
@@ -97,10 +96,10 @@
     "Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))) #>
 
   value (Binding.name "cterm") (Args.term >> (fn t =>
-  "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
+    "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
 
   value (Binding.name "cprop") (Args.prop >> (fn t =>
-  "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
+    "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
 
   value (Binding.name "cpat")
     (Args.context --
@@ -185,13 +184,24 @@
 
 (* outer syntax *)
 
+fun with_keyword f =
+  Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) =>
+    (f (name, Thy_Header.the_keyword thy name)
+      handle ERROR msg => error (msg ^ Position.str_of pos)));
+
 val _ = Context.>> (Context.map_theory
-  (value (Binding.name "keyword")
-    (Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) =>
-      (if is_none (Thy_Header.the_keyword thy name) then
-        ML_Syntax.atomic ("Parse.$$$ " ^ ML_Syntax.print_string name)
-       else error ("Unknown minor keyword " ^ quote name))
-      handle ERROR msg => error (msg ^ Position.str_of pos)))));
+ (value (Binding.name "keyword")
+    (with_keyword
+      (fn (name, NONE) => "Parse.$$$ " ^ ML_Syntax.print_string name
+        | (name, SOME _) => error ("Expected minor keyword " ^ quote name))) #>
+  value (Binding.name "command_spec")
+    (with_keyword
+      (fn (name, SOME kind) =>
+          "Keyword.command_spec " ^ ML_Syntax.atomic
+            (ML_Syntax.print_pair ML_Syntax.print_string
+              (ML_Syntax.print_pair ML_Syntax.print_string
+                (ML_Syntax.print_list ML_Syntax.print_string)) (name, kind))
+        | (name, NONE) => error ("Expected command keyword " ^ quote name)))));
 
 end;
 
diff -r 0c8fb96cce73 -r daf5538144d6 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Pure/Proof/extraction.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -820,25 +820,24 @@
 val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") [];
 
 val _ =
-  Outer_Syntax.command "realizers"
-  "specify realizers for primitive axioms / theorems, together with correctness proof"
-  Keyword.thy_decl
+  Outer_Syntax.command ("realizers", Keyword.thy_decl)
+    "specify realizers for primitive axioms / theorems, together with correctness proof"
     (Scan.repeat1 (Parse.xname -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
      (fn xs => Toplevel.theory (fn thy => add_realizers
        (map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy)));
 
 val _ =
-  Outer_Syntax.command "realizability"
-  "add equations characterizing realizability" Keyword.thy_decl
-  (Scan.repeat1 Parse.string >> (Toplevel.theory o add_realizes_eqns));
+  Outer_Syntax.command ("realizability", Keyword.thy_decl)
+    "add equations characterizing realizability"
+    (Scan.repeat1 Parse.string >> (Toplevel.theory o add_realizes_eqns));
 
 val _ =
-  Outer_Syntax.command "extract_type"
-  "add equations characterizing type of extracted program" Keyword.thy_decl
-  (Scan.repeat1 Parse.string >> (Toplevel.theory o add_typeof_eqns));
+  Outer_Syntax.command ("extract_type", Keyword.thy_decl)
+    "add equations characterizing type of extracted program"
+    (Scan.repeat1 Parse.string >> (Toplevel.theory o add_typeof_eqns));
 
 val _ =
-  Outer_Syntax.command "extract" "extract terms from proofs" Keyword.thy_decl
+  Outer_Syntax.command ("extract", Keyword.thy_decl) "extract terms from proofs"
     (Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
       extract (map (apfst (Global_Theory.get_thm thy)) xs) thy)));
 
diff -r 0c8fb96cce73 -r daf5538144d6 src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -189,31 +189,31 @@
 (* additional outer syntax for Isar *)
 
 val _ =
-  Outer_Syntax.improper_command "ProofGeneral.pr" "print state (internal)" Keyword.diag
+  Outer_Syntax.improper_command ("ProofGeneral.pr", Keyword.diag) "print state (internal)"
     (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
       if Toplevel.is_toplevel state orelse Toplevel.is_theory state then tell_clear_goals ()
       else (Toplevel.quiet := false; Toplevel.print_state true state))));
 
 val _ = (*undo without output -- historical*)
-  Outer_Syntax.improper_command "ProofGeneral.undo" "(internal)" Keyword.control
+  Outer_Syntax.improper_command ("ProofGeneral.undo", Keyword.control) "(internal)"
     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1)));
 
 val _ =
-  Outer_Syntax.improper_command "ProofGeneral.restart" "(internal)" Keyword.control
+  Outer_Syntax.improper_command ("ProofGeneral.restart", Keyword.control) "(internal)"
     (Parse.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
 
 val _ =
-  Outer_Syntax.improper_command "ProofGeneral.kill_proof" "(internal)" Keyword.control
+  Outer_Syntax.improper_command ("ProofGeneral.kill_proof", Keyword.control) "(internal)"
     (Scan.succeed (Toplevel.no_timing o
       Toplevel.imperative (fn () => (Isar.kill_proof (); tell_clear_goals ()))));
 
 val _ =
-  Outer_Syntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" Keyword.control
+  Outer_Syntax.improper_command ("ProofGeneral.inform_file_processed", Keyword.control) "(internal)"
     (Parse.name >> (fn file =>
       Toplevel.no_timing o Toplevel.imperative (fn () => inform_file_processed file)));
 
 val _ =
-  Outer_Syntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" Keyword.control
+  Outer_Syntax.improper_command ("ProofGeneral.inform_file_retracted", Keyword.control) "(internal)"
     (Parse.name >> (Toplevel.no_timing oo
       (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
 
diff -r 0c8fb96cce73 -r daf5538144d6 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -1032,7 +1032,7 @@
 (* Extra command for embedding prover-control inside document (obscure/debug usage). *)
 
 val _ =
-  Outer_Syntax.improper_command "ProofGeneral.process_pgip" "(internal)" Keyword.control
+  Outer_Syntax.improper_command ("ProofGeneral.process_pgip", Keyword.control) "(internal)"
     (Parse.text >> (Toplevel.no_timing oo
       (fn txt => Toplevel.imperative (fn () =>
         if print_mode_active proof_general_emacsN
diff -r 0c8fb96cce73 -r daf5538144d6 src/Pure/System/isar.ML
--- a/src/Pure/System/isar.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Pure/System/isar.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -164,35 +164,36 @@
 (* global history *)
 
 val _ =
-  Outer_Syntax.improper_command "init_toplevel" "init toplevel point-of-interest" Keyword.control
+  Outer_Syntax.improper_command ("init_toplevel", Keyword.control) "init toplevel point-of-interest"
     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative init));
 
 val _ =
-  Outer_Syntax.improper_command "linear_undo" "undo commands" Keyword.control
+  Outer_Syntax.improper_command ("linear_undo", Keyword.control) "undo commands"
     (Scan.optional Parse.nat 1 >>
       (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => linear_undo n)));
 
 val _ =
-  Outer_Syntax.improper_command "undo" "undo commands (skipping closed proofs)" Keyword.control
+  Outer_Syntax.improper_command ("undo", Keyword.control) "undo commands (skipping closed proofs)"
     (Scan.optional Parse.nat 1 >>
       (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => undo n)));
 
 val _ =
-  Outer_Syntax.improper_command "undos_proof" "undo commands (skipping closed proofs)"
-    Keyword.control
+  Outer_Syntax.improper_command ("undos_proof", Keyword.control)
+    "undo commands (skipping closed proofs)"
     (Scan.optional Parse.nat 1 >> (fn n => Toplevel.no_timing o
       Toplevel.keep (fn state =>
         if Toplevel.is_proof state then (undo n; print ()) else raise Toplevel.UNDEF)));
 
 val _ =
-  Outer_Syntax.improper_command "cannot_undo" "partial undo -- Proof General legacy"
-    Keyword.control
+  Outer_Syntax.improper_command ("cannot_undo", Keyword.control)
+    "partial undo -- Proof General legacy"
     (Parse.name >>
       (fn "end" => Toplevel.no_timing o Toplevel.imperative (fn () => undo 1)
         | txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt))));
 
 val _ =
-  Outer_Syntax.improper_command "kill" "kill partial proof or theory development" Keyword.control
+  Outer_Syntax.improper_command ("kill", Keyword.control)
+    "kill partial proof or theory development"
     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
 
 end;
diff -r 0c8fb96cce73 -r daf5538144d6 src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Pure/System/session.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -48,7 +48,7 @@
     (if Distribution.changelog <> "" then "\nSee also " ^ Distribution.changelog else "");
 
 val _ =
-  Outer_Syntax.improper_command "welcome" "print welcome message" Keyword.diag
+  Outer_Syntax.improper_command ("welcome", Keyword.diag) "print welcome message"
     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (writeln o welcome)));
 
 
diff -r 0c8fb96cce73 -r daf5538144d6 src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Pure/Thy/thy_header.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -8,13 +8,13 @@
 sig
   type header =
    {name: string, imports: string list,
-    keywords: (string * (string * string list) option) list,
+    keywords: (string * Keyword.spec option) list,
     uses: (Path.T * bool) list}
-  val make: string -> string list -> (string * (string * string list) option) list ->
+  val make: string -> string list -> (string * Keyword.spec option) list ->
     (Path.T * bool) list -> header
   val define_keywords: header -> unit
-  val declare_keyword: string * (string * string list) option -> theory -> theory
-  val the_keyword: theory -> string -> Keyword.T option
+  val declare_keyword: string * Keyword.spec option -> theory -> theory
+  val the_keyword: theory -> string -> Keyword.spec option
   val args: header parser
   val read: Position.T -> string -> header
 end;
@@ -24,7 +24,7 @@
 
 type header =
  {name: string, imports: string list,
-  keywords: (string * (string * string list) option) list,
+  keywords: (string * Keyword.spec option) list,
   uses: (Path.T * bool) list};
 
 fun make name imports keywords uses : header =
@@ -35,26 +35,27 @@
 (** keyword declarations **)
 
 fun define_keywords ({keywords, ...}: header) =
-  List.app (fn (name, decl) => Keyword.define (name, Option.map Keyword.make decl)) keywords;
+  List.app (Keyword.define o apsnd (Option.map Keyword.spec)) keywords;
 
 fun err_dup name = error ("Inconsistent declaration of outer syntax keyword " ^ quote name);
 
 structure Data = Theory_Data
 (
-  type T = Keyword.T option Symtab.table;
+  type T = Keyword.spec option Symtab.table;
   val empty = Symtab.empty;
   val extend = I;
   fun merge data : T = Symtab.merge (op =) data handle Symtab.DUP name => err_dup name;
 );
 
-fun declare_keyword (name, decl) = Data.map (fn data =>
-  let val kind = Option.map Keyword.make decl
-  in Symtab.update_new (name, kind) data handle Symtab.DUP name => err_dup name end);
+fun declare_keyword (name, spec) =
+  Data.map (fn data =>
+    (Option.map Keyword.spec spec;
+      Symtab.update_new (name, spec) data handle Symtab.DUP dup => err_dup dup));
 
 fun the_keyword thy name =
   (case Symtab.lookup (Data.get thy) name of
-    SOME kind => kind
-  | NONE => error ("Unknown outer syntax keyword " ^ quote name));
+    SOME spec => spec
+  | NONE => error ("Undeclared outer syntax keyword " ^ quote name));
 
 
 
diff -r 0c8fb96cce73 -r daf5538144d6 src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Pure/Tools/find_consts.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -135,7 +135,7 @@
 in
 
 val _ =
-  Outer_Syntax.improper_command "find_consts" "search constants by type pattern" Keyword.diag
+  Outer_Syntax.improper_command ("find_consts", Keyword.diag) "search constants by type pattern"
     (Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion)
       >> (fn spec => Toplevel.no_timing o
         Toplevel.keep (fn state => find_consts (Toplevel.context_of state) spec)));
diff -r 0c8fb96cce73 -r daf5538144d6 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Pure/Tools/find_theorems.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -612,8 +612,8 @@
 val query_parser = Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion));
 
 val _ =
-  Outer_Syntax.improper_command "find_theorems" "print theorems meeting specified criteria"
-    Keyword.diag
+  Outer_Syntax.improper_command ("find_theorems", Keyword.diag)
+    "print theorems meeting specified criteria"
     (options -- query_parser
       >> (fn ((opt_lim, rem_dups), spec) =>
         Toplevel.no_timing o
diff -r 0c8fb96cce73 -r daf5538144d6 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Tools/Code/code_haskell.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -449,10 +449,9 @@
 (** Isar setup **)
 
 val _ =
-  Outer_Syntax.command "code_monad" "define code syntax for monads" Keyword.thy_decl (
-    Parse.term_group -- Parse.name >> (fn (raw_bind, target) =>
-      Toplevel.theory  (add_monad target raw_bind))
-  );
+  Outer_Syntax.command @{command_spec "code_monad"} "define code syntax for monads"
+    (Parse.term_group -- Parse.name >> (fn (raw_bind, target) =>
+      Toplevel.theory  (add_monad target raw_bind)));
 
 val setup =
   Code_Target.add_target
diff -r 0c8fb96cce73 -r daf5538144d6 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Tools/Code/code_preproc.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -525,8 +525,8 @@
   end;
 
 val _ =
-  Outer_Syntax.improper_command "print_codeproc" "print code preprocessor setup"
-  Keyword.diag (Scan.succeed
+  Outer_Syntax.improper_command @{command_spec "print_codeproc"} "print code preprocessor setup"
+    (Scan.succeed
       (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
         (print_codeproc o Toplevel.theory_of)));
 
diff -r 0c8fb96cce73 -r daf5538144d6 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Tools/Code/code_runtime.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -352,13 +352,14 @@
 in
 
 val _ =
-  Outer_Syntax.command "code_reflect" "enrich runtime environment with generated code"
-    Keyword.thy_decl (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- (parse_datatype
+  Outer_Syntax.command @{command_spec "code_reflect"}
+    "enrich runtime environment with generated code"
+    (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)));
+    >> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory
+      (code_reflect_cmd raw_datatypes raw_functions module_name some_file)));
 
 end; (*local*)
 
diff -r 0c8fb96cce73 -r daf5538144d6 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Tools/Code/code_target.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -680,57 +680,54 @@
        -- code_expr_argsP) >> (fn seris => export_code_cmd raw_cs seris)));
 
 val _ =
-  Outer_Syntax.command "code_class" "define code syntax for class" Keyword.thy_decl (
-    process_multi_syntax Parse.xname (Scan.option Parse.string)
-    add_class_syntax_cmd);
+  Outer_Syntax.command @{command_spec "code_class"} "define code syntax for class"
+    (process_multi_syntax Parse.xname (Scan.option Parse.string)
+      add_class_syntax_cmd);
 
 val _ =
-  Outer_Syntax.command "code_instance" "define code syntax for instance" Keyword.thy_decl (
-    process_multi_syntax (Parse.xname --| @{keyword "::"} -- Parse.xname)
+  Outer_Syntax.command @{command_spec "code_instance"} "define code syntax for instance"
+    (process_multi_syntax (Parse.xname --| @{keyword "::"} -- Parse.xname)
       (Scan.option (Parse.minus >> K ()))
-    add_instance_syntax_cmd);
+      add_instance_syntax_cmd);
 
 val _ =
-  Outer_Syntax.command "code_type" "define code syntax for type constructor" Keyword.thy_decl (
-    process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax
-    add_tyco_syntax_cmd);
+  Outer_Syntax.command @{command_spec "code_type"} "define code syntax for type constructor"
+    (process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax
+      add_tyco_syntax_cmd);
 
 val _ =
-  Outer_Syntax.command "code_const" "define code syntax for constant" Keyword.thy_decl (
-    process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax
-    add_const_syntax_cmd);
+  Outer_Syntax.command @{command_spec "code_const"} "define code syntax for constant"
+    (process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax
+      add_const_syntax_cmd);
 
 val _ =
-  Outer_Syntax.command "code_reserved" "declare words as reserved for target language"
-    Keyword.thy_decl (
-    Parse.name -- Scan.repeat1 Parse.name
-    >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds)
-  );
+  Outer_Syntax.command @{command_spec "code_reserved"}
+    "declare words as reserved for target language"
+    (Parse.name -- Scan.repeat1 Parse.name
+      >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds));
 
 val _ =
-  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 (@{keyword "attach"} |-- Scan.repeat1 Parse.term) [] >> pair s >> SOME))
-    >> (fn ((target, name), content_consts) =>
-        (Toplevel.theory o add_include_cmd target) (name, content_consts))
-  );
+  Outer_Syntax.command @{command_spec "code_include"}
+    "declare piece of code to be included in generated code"
+    (Parse.name -- Parse.name -- (Parse.text :|--
+      (fn "-" => Scan.succeed NONE
+        | 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)));
 
 val _ =
-  Outer_Syntax.command "code_modulename" "alias module to other name" Keyword.thy_decl (
-    Parse.name -- Scan.repeat1 (Parse.name -- Parse.name)
-    >> (fn (target, modlnames) => (Toplevel.theory o fold (add_module_alias target)) modlnames)
-  );
+  Outer_Syntax.command @{command_spec "code_modulename"} "alias module to other name"
+    (Parse.name -- Scan.repeat1 (Parse.name -- Parse.name)
+      >> (fn (target, modlnames) => (Toplevel.theory o fold (add_module_alias target)) modlnames));
 
 val _ =
-  Outer_Syntax.command "code_abort" "permit constant to be implemented as program abort"
-    Keyword.thy_decl (
-    Scan.repeat1 Parse.term_group >> (Toplevel.theory o fold allow_abort_cmd)
-  );
+  Outer_Syntax.command @{command_spec "code_abort"}
+    "permit constant to be implemented as program abort"
+    (Scan.repeat1 Parse.term_group >> (Toplevel.theory o fold allow_abort_cmd));
 
 val _ =
-  Outer_Syntax.command "export_code" "generate executable code for constants"
-    Keyword.diag (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
+  Outer_Syntax.command @{command_spec "export_code"} "generate executable code for constants"
+    (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
 
 end; (*local*)
 
diff -r 0c8fb96cce73 -r daf5538144d6 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Tools/Code/code_thingol.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -1046,14 +1046,15 @@
 in
 
 val _ =
-  Outer_Syntax.improper_command "code_thms" "print system of code equations for code" Keyword.diag
+  Outer_Syntax.improper_command @{command_spec "code_thms"}
+    "print system of code equations for code"
     (Scan.repeat1 Parse.term_group
       >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
         o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
 
 val _ =
-  Outer_Syntax.improper_command "code_deps" "visualize dependencies of code equations for code"
-    Keyword.diag
+  Outer_Syntax.improper_command @{command_spec "code_deps"}
+    "visualize dependencies of code equations for code"
     (Scan.repeat1 Parse.term_group
       >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
         o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
diff -r 0c8fb96cce73 -r daf5538144d6 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Tools/induct.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -259,8 +259,9 @@
   end;
 
 val _ =
-  Outer_Syntax.improper_command "print_induct_rules" "print induction and cases rules"
-    Keyword.diag (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+  Outer_Syntax.improper_command @{command_spec "print_induct_rules"}
+    "print induction and cases rules"
+    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
       Toplevel.keep (print_rules o Toplevel.context_of)));
 
 
diff -r 0c8fb96cce73 -r daf5538144d6 src/Tools/interpretation_with_defs.ML
--- a/src/Tools/interpretation_with_defs.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Tools/interpretation_with_defs.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -80,8 +80,8 @@
 end;
 
 val _ =
-  Outer_Syntax.command "interpretation"
-    "prove interpretation of locale expression in theory" Keyword.thy_goal
+  Outer_Syntax.command @{command_spec "interpretation"}
+    "prove interpretation of locale expression in theory"
     (Parse.!!! (Parse_Spec.locale_expression true) --
       Scan.optional (@{keyword "defines"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
         -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "is"} -- Parse.term))) [] --
diff -r 0c8fb96cce73 -r daf5538144d6 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Tools/quickcheck.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -83,7 +83,6 @@
 struct
 
 val quickcheckN = "quickcheck"
-val quickcheck_paramsN = "quickcheck_params"
 
 val genuineN = "genuine"
 val noneN = "none"
@@ -530,11 +529,12 @@
   @{keyword "["} |-- Parse.list1 parse_arg --| @{keyword "]"} || Scan.succeed [];
 
 val _ =
-  Outer_Syntax.command quickcheck_paramsN "set parameters for random testing" Keyword.thy_decl
+  Outer_Syntax.command @{command_spec "quickcheck_params"} "set parameters for random testing"
     (parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args)));
 
 val _ =
-  Outer_Syntax.improper_command quickcheckN "try to find counterexample for subgoal" Keyword.diag
+  Outer_Syntax.improper_command @{command_spec "quickcheck"}
+    "try to find counterexample for subgoal"
     (parse_args -- Scan.optional Parse.nat 1
       >> (fn (args, i) => Toplevel.no_timing o Toplevel.keep (quickcheck_cmd args i)));
 
diff -r 0c8fb96cce73 -r daf5538144d6 src/Tools/solve_direct.ML
--- a/src/Tools/solve_direct.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Tools/solve_direct.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -107,10 +107,9 @@
 val solve_direct = do_solve_direct Normal
 
 val _ =
-  Outer_Syntax.improper_command solve_directN
-    "try to solve conjectures directly with existing theorems" Keyword.diag
-    (Scan.succeed
-      (Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
+  Outer_Syntax.improper_command @{command_spec "solve_direct"}
+    "try to solve conjectures directly with existing theorems"
+    (Scan.succeed (Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
 
 
 (* hook *)
diff -r 0c8fb96cce73 -r daf5538144d6 src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Tools/subtyping.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -1028,10 +1028,10 @@
 (* outer syntax commands *)
 
 val _ =
-  Outer_Syntax.improper_command "print_coercions" "print all coercions" Keyword.diag
+  Outer_Syntax.improper_command @{command_spec "print_coercions"} "print all coercions"
     (Scan.succeed (Toplevel.keep (print_coercions o Toplevel.context_of)))
 val _ =
-  Outer_Syntax.improper_command "print_coercion_maps" "print all coercion maps" Keyword.diag
+  Outer_Syntax.improper_command @{command_spec "print_coercion_maps"} "print all coercion maps"
     (Scan.succeed (Toplevel.keep (print_coercion_maps o Toplevel.context_of)))
 
 end;
diff -r 0c8fb96cce73 -r daf5538144d6 src/Tools/try.ML
--- a/src/Tools/try.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Tools/try.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -88,9 +88,9 @@
     |> tap (fn NONE => Output.urgent_message "Tried in vain." | _ => ())
 
 val _ =
-  Outer_Syntax.improper_command tryN
-      "try a combination of automatic proving and disproving tools" Keyword.diag
-      (Scan.succeed (Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
+  Outer_Syntax.improper_command @{command_spec "try"}
+    "try a combination of automatic proving and disproving tools"
+    (Scan.succeed (Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
 
 
 (* automatic try *)
diff -r 0c8fb96cce73 -r daf5538144d6 src/Tools/value.ML
--- a/src/Tools/value.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Tools/value.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -63,7 +63,7 @@
   Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"})
   
 val _ =
-  Outer_Syntax.improper_command "value" "evaluate and print term" Keyword.diag
+  Outer_Syntax.improper_command @{command_spec "value"} "evaluate and print term"
     (opt_evaluator -- opt_modes -- Parse.term
       >> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep
           (value_cmd some_name modes t)));
diff -r 0c8fb96cce73 -r daf5538144d6 src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/ZF/Tools/datatype_package.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -430,19 +430,18 @@
   Parse.name -- Scan.optional (@{keyword "("} |-- Parse.list1 Parse.term --| @{keyword ")"}) [] --
     Parse.opt_mixfix >> Parse.triple1;
 
-val datatype_decl =
-  (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 "";
 
 val _ =
-  Outer_Syntax.command (coind_prefix ^ "datatype")
-    ("define " ^ coind_prefix ^ "datatype") Keyword.thy_decl datatype_decl;
+  Outer_Syntax.command
+    (if coind then @{command_spec "codatatype"} else @{command_spec "datatype"})
+    ("define " ^ coind_prefix ^ "datatype")
+    ((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));
 
 end;
 
diff -r 0c8fb96cce73 -r daf5538144d6 src/ZF/Tools/ind_cases.ML
--- a/src/ZF/Tools/ind_cases.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/ZF/Tools/ind_cases.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -65,8 +65,8 @@
 (* outer syntax *)
 
 val _ =
-  Outer_Syntax.command "inductive_cases"
-    "create simplified instances of elimination rules (improper)" Keyword.thy_script
+  Outer_Syntax.command @{command_spec "inductive_cases"}
+    "create simplified instances of elimination rules (improper)"
     (Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Scan.repeat1 Parse.prop)
       >> (Toplevel.theory o inductive_cases));
 
diff -r 0c8fb96cce73 -r daf5538144d6 src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/ZF/Tools/induct_tacs.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -188,16 +188,13 @@
 
 (* outer syntax *)
 
-val rep_datatype_decl =
-  (@{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 _ =
-  Outer_Syntax.command "rep_datatype" "represent existing set inductively" Keyword.thy_decl
-    (rep_datatype_decl >> Toplevel.theory);
+  Outer_Syntax.command @{command_spec "rep_datatype"} "represent existing set inductively"
+    ((@{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) => Toplevel.theory (rep_datatype x y z w)));
 
 end;
 
diff -r 0c8fb96cce73 -r daf5538144d6 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/ZF/Tools/inductive_package.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -591,8 +591,9 @@
   >> (Toplevel.theory o mk_ind);
 
 val _ =
-  Outer_Syntax.command (co_prefix ^ "inductive")
-    ("define " ^ co_prefix ^ "inductive sets") Keyword.thy_decl ind_decl;
+  Outer_Syntax.command
+    (if coind then @{command_spec "coinductive"} else @{command_spec "inductive"})
+    ("define " ^ co_prefix ^ "inductive sets") ind_decl;
 
 end;
 
diff -r 0c8fb96cce73 -r daf5538144d6 src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/ZF/Tools/primrec_package.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -196,8 +196,7 @@
 (* outer syntax *)
 
 val _ =
-  Outer_Syntax.command "primrec" "define primitive recursive functions on datatypes"
-    Keyword.thy_decl
+  Outer_Syntax.command @{command_spec "primrec"} "define primitive recursive functions on datatypes"
     (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)
       >> (Toplevel.theory o (#1 oo (add_primrec o map Parse.triple_swap))));
 
diff -r 0c8fb96cce73 -r daf5538144d6 src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Fri Mar 16 16:32:34 2012 +0000
+++ b/src/ZF/Tools/typechk.ML	Fri Mar 16 18:21:22 2012 +0100
@@ -121,7 +121,7 @@
     "ZF type-checking";
 
 val _ =
-  Outer_Syntax.improper_command "print_tcset" "print context of ZF typecheck" Keyword.diag
+  Outer_Syntax.improper_command @{command_spec "print_tcset"} "print context of ZF typecheck"
     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
       Toplevel.keep (print_tcset o Toplevel.context_of)));