# HG changeset patch
# User wenzelm
# Date 1331845733 -3600
# Node ID d0181abdbdac82469a6ee1ebd7ecf9314b93d7e4
# Parent  94aa7b81bcf69a77b653e623a2bb798c4d386b32
declare command keywords via theory header, including strict checking outside Pure;

diff -r 94aa7b81bcf6 -r d0181abdbdac src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/FOL/FOL.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -6,6 +6,7 @@
 
 theory FOL
 imports IFOL
+keywords "print_claset" "print_induct_rules" :: diag
 uses
   "~~/src/Provers/classical.ML"
   "~~/src/Provers/blast.ML"
diff -r 94aa7b81bcf6 -r d0181abdbdac src/HOL/Boogie/Boogie.thy
--- a/src/HOL/Boogie/Boogie.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Boogie/Boogie.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -6,6 +6,8 @@
 
 theory Boogie
 imports Word
+keywords
+  "boogie_open" "boogie_end" :: thy_decl and "boogie_vc" :: thy_goal and "boogie_status" :: diag
 uses
   ("Tools/boogie_vcs.ML")
   ("Tools/boogie_loader.ML")
diff -r 94aa7b81bcf6 -r d0181abdbdac src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Datatype.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -7,6 +7,7 @@
 
 theory Datatype
 imports Product_Type Sum_Type Nat
+keywords "datatype" :: thy_decl
 uses
   ("Tools/Datatype/datatype.ML")
   ("Tools/inductive_realizer.ML")
diff -r 94aa7b81bcf6 -r d0181abdbdac src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Fun.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -7,6 +7,7 @@
 
 theory Fun
 imports Complete_Lattices
+keywords "enriched_type" :: thy_goal
 uses ("Tools/enriched_type.ML")
 begin
 
diff -r 94aa7b81bcf6 -r d0181abdbdac src/HOL/FunDef.thy
--- a/src/HOL/FunDef.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/FunDef.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -6,6 +6,7 @@
 
 theory FunDef
 imports Partial_Function Wellfounded
+keywords "function" "termination" :: thy_goal and "fun" :: thy_decl
 uses
   "Tools/prop_logic.ML"
   "Tools/sat_solver.ML"
diff -r 94aa7b81bcf6 -r d0181abdbdac src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/HOL.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -6,6 +6,8 @@
 
 theory HOL
 imports Pure "~~/src/Tools/Code_Generator"
+keywords
+  "print_coercions" "print_coercion_maps" "print_claset" "print_induct_rules" :: diag
 uses
   ("Tools/hologic.ML")
   "~~/src/Tools/IsaPlanner/zipper.ML"
diff -r 94aa7b81bcf6 -r d0181abdbdac src/HOL/HOLCF/Cpodef.thy
--- a/src/HOL/HOLCF/Cpodef.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/HOLCF/Cpodef.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -6,6 +6,7 @@
 
 theory Cpodef
 imports Adm
+keywords "pcpodef" "cpodef" :: thy_goal
 uses ("Tools/cpodef.ML")
 begin
 
diff -r 94aa7b81bcf6 -r d0181abdbdac src/HOL/HOLCF/Domain.thy
--- a/src/HOL/HOLCF/Domain.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/HOLCF/Domain.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -6,7 +6,9 @@
 
 theory Domain
 imports Representable Domain_Aux
-keywords "lazy" "unsafe"
+keywords
+  "domaindef" :: thy_decl and "lazy" "unsafe" and
+  "domain_isomorphism" "domain" :: thy_decl
 uses
   ("Tools/domaindef.ML")
   ("Tools/Domain/domain_isomorphism.ML")
diff -r 94aa7b81bcf6 -r d0181abdbdac src/HOL/HOLCF/Fixrec.thy
--- a/src/HOL/HOLCF/Fixrec.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/HOLCF/Fixrec.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -6,6 +6,7 @@
 
 theory Fixrec
 imports Plain_HOLCF
+keywords "fixrec" :: thy_decl
 uses
   ("Tools/holcf_library.ML")
   ("Tools/fixrec.ML")
diff -r 94aa7b81bcf6 -r d0181abdbdac src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -7,6 +7,7 @@
 
 theory Hilbert_Choice
 imports Nat Wellfounded Plain
+keywords "specification" "ax_specification" :: thy_goal
 uses ("Tools/choice_specification.ML")
 begin
 
diff -r 94aa7b81bcf6 -r d0181abdbdac src/HOL/Import/Importer.thy
--- a/src/HOL/Import/Importer.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Import/Importer.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -4,7 +4,10 @@
 
 theory Importer
 imports Main
-keywords ">"
+keywords
+  "import_segment" "import_theory" "end_import" "setup_theory" "end_setup"
+  "setup_dump" "append_dump" "flush_dump" "ignore_thms" "type_maps"
+  "def_maps" "thm_maps" "const_renames" "const_moves" "const_maps" :: thy_decl and ">"
 uses "shuffler.ML" "import_rews.ML" ("proof_kernel.ML") ("replay.ML") ("import.ML")
 begin
 
diff -r 94aa7b81bcf6 -r d0181abdbdac src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Inductive.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -6,7 +6,11 @@
 
 theory Inductive 
 imports Complete_Lattices
-keywords "monos"
+keywords
+  "inductive" "coinductive" :: thy_decl and
+  "inductive_cases" "inductive_simps" :: thy_script and "monos" and
+  "rep_datatype" :: thy_goal and
+  "primrec" :: thy_decl
 uses
   "Tools/dseq.ML"
   ("Tools/inductive.ML")
diff -r 94aa7b81bcf6 -r d0181abdbdac src/HOL/Library/Old_Recdef.thy
--- a/src/HOL/Library/Old_Recdef.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Library/Old_Recdef.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -6,7 +6,10 @@
 
 theory Old_Recdef
 imports Wfrec
-keywords "recdef" :: thy_decl and "permissive" "congs" "hints"
+keywords
+  "recdef" "defer_recdef" :: thy_decl and
+  "recdef_tc" :: thy_goal and
+  "permissive" "congs" "hints"
 uses
   ("~~/src/HOL/Tools/TFL/casesplit.ML")
   ("~~/src/HOL/Tools/TFL/utils.ML")
diff -r 94aa7b81bcf6 -r d0181abdbdac src/HOL/Metis.thy
--- a/src/HOL/Metis.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Metis.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -8,6 +8,7 @@
 
 theory Metis
 imports ATP
+keywords "try0" :: diag
 uses "~~/src/Tools/Metis/metis.ML"
      ("Tools/Metis/metis_generate.ML")
      ("Tools/Metis/metis_reconstruct.ML")
diff -r 94aa7b81bcf6 -r d0181abdbdac src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Nitpick.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -9,6 +9,7 @@
 
 theory Nitpick
 imports Map Quotient SAT Record
+keywords "nitpick" :: diag and "nitpick_params" :: thy_decl
 uses ("Tools/Nitpick/kodkod.ML")
      ("Tools/Nitpick/kodkod_sat.ML")
      ("Tools/Nitpick/nitpick_util.ML")
diff -r 94aa7b81bcf6 -r d0181abdbdac src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -1,6 +1,9 @@
 theory Nominal 
 imports Main "~~/src/HOL/Library/Infinite_Set"
-keywords "avoids"
+keywords
+  "atom_decl" "nominal_datatype" "equivariance" :: thy_decl and
+  "nominal_primrec" "nominal_inductive" "nominal_inductive2" :: thy_goal and
+  "avoids"
 uses
   ("nominal_thmdecls.ML")
   ("nominal_atoms.ML")
diff -r 94aa7b81bcf6 -r d0181abdbdac src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Orderings.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -6,6 +6,7 @@
 
 theory Orderings
 imports HOL
+keywords "print_orders" :: diag
 uses
   "~~/src/Provers/order.ML"
   "~~/src/Provers/quasi.ML"  (* FIXME unused? *)
diff -r 94aa7b81bcf6 -r d0181abdbdac src/HOL/Partial_Function.thy
--- a/src/HOL/Partial_Function.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Partial_Function.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -6,6 +6,7 @@
 
 theory Partial_Function
 imports Complete_Partial_Order Option
+keywords "partial_function" :: thy_decl
 uses 
   "Tools/Function/function_lib.ML" 
   "Tools/Function/partial_function.ML" 
diff -r 94aa7b81bcf6 -r d0181abdbdac src/HOL/Predicate_Compile.thy
--- a/src/HOL/Predicate_Compile.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Predicate_Compile.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -6,6 +6,7 @@
 
 theory Predicate_Compile
 imports Predicate New_Random_Sequence Quickcheck_Exhaustive
+keywords "code_pred" :: thy_goal and "values" :: diag
 uses
   "Tools/Predicate_Compile/predicate_compile_aux.ML"
   "Tools/Predicate_Compile/predicate_compile_compilations.ML"
diff -r 94aa7b81bcf6 -r d0181abdbdac src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Product_Type.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -7,6 +7,7 @@
 
 theory Product_Type
 imports Typedef Inductive Fun
+keywords "inductive_set" "coinductive_set" :: thy_decl
 uses
   ("Tools/split_rule.ML")
   ("Tools/inductive_set.ML")
diff -r 94aa7b81bcf6 -r d0181abdbdac src/HOL/Quickcheck_Exhaustive.thy
--- a/src/HOL/Quickcheck_Exhaustive.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -4,6 +4,7 @@
 
 theory Quickcheck_Exhaustive
 imports Quickcheck
+keywords "quickcheck_generator" :: thy_decl
 uses
   ("Tools/Quickcheck/exhaustive_generators.ML")
   ("Tools/Quickcheck/abstract_generators.ML")
diff -r 94aa7b81bcf6 -r d0181abdbdac src/HOL/Quickcheck_Narrowing.thy
--- a/src/HOL/Quickcheck_Narrowing.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Quickcheck_Narrowing.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -4,6 +4,7 @@
 
 theory Quickcheck_Narrowing
 imports Quickcheck_Exhaustive
+keywords "find_unused_assms" :: diag
 uses
   ("Tools/Quickcheck/PNF_Narrowing_Engine.hs")
   ("Tools/Quickcheck/Narrowing_Engine.hs")
diff -r 94aa7b81bcf6 -r d0181abdbdac src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Quotient.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -6,7 +6,10 @@
 
 theory Quotient
 imports Plain Hilbert_Choice Equiv_Relations
-keywords "/"
+keywords
+  "print_quotmaps" "print_quotients" "print_quotconsts" :: diag and
+  "quotient_type" :: thy_goal and "/" and
+  "quotient_definition" :: thy_decl
 uses
   ("Tools/Quotient/quotient_info.ML")
   ("Tools/Quotient/quotient_type.ML")
diff -r 94aa7b81bcf6 -r d0181abdbdac src/HOL/Record.thy
--- a/src/HOL/Record.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Record.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -10,6 +10,7 @@
 
 theory Record
 imports Plain Quickcheck_Narrowing
+keywords "record" :: thy_decl
 uses ("Tools/record.ML")
 begin
 
diff -r 94aa7b81bcf6 -r d0181abdbdac src/HOL/Refute.thy
--- a/src/HOL/Refute.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Refute.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -9,6 +9,7 @@
 
 theory Refute
 imports Hilbert_Choice List Sledgehammer
+keywords "refute" :: diag and "refute_params" :: thy_decl
 uses "Tools/refute.ML"
 begin
 
diff -r 94aa7b81bcf6 -r d0181abdbdac src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/SMT.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -6,6 +6,7 @@
 
 theory SMT
 imports Record
+keywords "smt_status" :: diag
 uses
   "Tools/SMT/smt_utils.ML"
   "Tools/SMT/smt_failure.ML"
diff -r 94aa7b81bcf6 -r d0181abdbdac src/HOL/SPARK/SPARK_Setup.thy
--- a/src/HOL/SPARK/SPARK_Setup.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/SPARK/SPARK_Setup.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -7,6 +7,9 @@
 
 theory SPARK_Setup
 imports Word
+keywords
+  "spark_open" "spark_proof_functions" "spark_types" "spark_end" :: thy_decl and
+  "spark_vc" :: thy_goal and "spark_status" :: diag
 uses
   "Tools/fdl_lexer.ML"
   "Tools/fdl_parser.ML"
diff -r 94aa7b81bcf6 -r d0181abdbdac src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Sledgehammer.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -8,6 +8,7 @@
 
 theory Sledgehammer
 imports ATP SMT
+keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl
 uses "Tools/Sledgehammer/async_manager.ML"
      "Tools/Sledgehammer/sledgehammer_util.ML"
      "Tools/Sledgehammer/sledgehammer_filter.ML"
diff -r 94aa7b81bcf6 -r d0181abdbdac src/HOL/Statespace/StateSpaceLocale.thy
--- a/src/HOL/Statespace/StateSpaceLocale.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Statespace/StateSpaceLocale.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -5,6 +5,7 @@
 header {* Setup for State Space Locales \label{sec:StateSpaceLocale}*}
 
 theory StateSpaceLocale imports StateFun 
+keywords "statespace" :: thy_decl
 uses "state_space.ML" "state_fun.ML"
 begin
 
diff -r 94aa7b81bcf6 -r d0181abdbdac src/HOL/TPTP/TPTP_Parser.thy
--- a/src/HOL/TPTP/TPTP_Parser.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Parser.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -9,6 +9,7 @@
 
 theory TPTP_Parser
 imports Main
+keywords "import_tptp" :: diag (* FIXME !? *) 
 uses
   "TPTP_Parser/ml_yacc_lib.ML" (*generated from ML-Yacc's lib*)
 
diff -r 94aa7b81bcf6 -r d0181abdbdac src/HOL/Typedef.thy
--- a/src/HOL/Typedef.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Typedef.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -6,7 +6,7 @@
 
 theory Typedef
 imports Set
-keywords "morphisms"
+keywords "typedef" :: thy_goal and "morphisms"
 uses ("Tools/typedef.ML")
 begin
 
diff -r 94aa7b81bcf6 -r d0181abdbdac src/HOL/ex/Interpretation_with_Defs.thy
--- a/src/HOL/ex/Interpretation_with_Defs.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/ex/Interpretation_with_Defs.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -6,6 +6,7 @@
 
 theory Interpretation_with_Defs
 imports Pure
+keywords "interpretation" :: thy_goal
 uses "~~/src/Tools/interpretation_with_defs.ML"
 begin
 
diff -r 94aa7b81bcf6 -r d0181abdbdac src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Mar 15 22:08:53 2012 +0100
@@ -21,7 +21,7 @@
     "constrains", "defines", "fixes", "for", "identifier", "if",
     "imports", "in", "infix", "infixl", "infixr", "is", "keywords",
     "notes", "obtains", "open", "output", "overloaded", "pervasive",
-    "shows", "structure", "unchecked", "uses", "where", "|", "by"]));
+    "shows", "structure", "unchecked", "uses", "where", "|"]));
 
 
 
diff -r 94aa7b81bcf6 -r d0181abdbdac src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/Pure/Isar/keyword.ML	Thu Mar 15 22:08:53 2012 +0100
@@ -48,7 +48,7 @@
   val status: unit -> unit
   val keyword: string -> unit
   val command: string -> T -> unit
-  val declare: string * (string * string list) option -> unit
+  val declare: string -> T option -> unit
   val is_diag: string -> bool
   val is_control: string -> bool
   val is_regular: string -> bool
@@ -215,8 +215,8 @@
   change_commands (Symtab.update (name, kind));
   command_status (name, kind));
 
-fun declare (name, NONE) = keyword name
-  | declare (name, SOME kind) = command name (make kind);
+fun declare name NONE = keyword name
+  | declare name (SOME kind) = command name kind;
 
 
 (* command categories *)
diff -r 94aa7b81bcf6 -r d0181abdbdac src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Mar 15 22:08:53 2012 +0100
@@ -123,11 +123,23 @@
 val global_outer_syntax = Unsynchronized.ref empty_outer_syntax;
 
 fun add_command name kind cmd = CRITICAL (fn () =>
- (Keyword.command name kind;
-  Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
-   (if not (Symtab.defined commands name) then ()
-    else warning ("Redefining outer syntax command " ^ quote name);
-    Symtab.update (name, cmd) commands)))));
+  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 ()
+          else error ("Inconsistent outer syntax keyword declaration " ^ quote name)
+      | NONE =>
+          (Keyword.command name kind;
+           if Context.theory_name thy = Context.PureN then ()
+           else error ("Undeclared outer syntax command " ^ quote name)));
+  in
+    Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
+     (if not (Symtab.defined commands name) then ()
+      else warning ("Redefining outer syntax command " ^ quote name);
+      Symtab.update (name, cmd) commands)))
+  end);
 
 in
 
diff -r 94aa7b81bcf6 -r d0181abdbdac src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/Pure/PIDE/document.ML	Thu Mar 15 22:08:53 2012 +0100
@@ -215,7 +215,8 @@
           val imports = (case header of Exn.Res (_, {imports, ...}) => imports | _ => []);
           val keywords = (case header of Exn.Res (_, {keywords, ...}) => keywords | _ => []);
           val header' =
-            (List.app Keyword.declare keywords; header)
+            (List.app (fn (name, decl) =>
+                Keyword.declare name (Option.map Keyword.make decl)) keywords; header)
               handle exn as ERROR _ => Exn.Exn exn;
           val nodes1 = nodes
             |> default_node name
diff -r 94aa7b81bcf6 -r d0181abdbdac src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/Pure/Thy/thy_header.ML	Thu Mar 15 22:08:53 2012 +0100
@@ -43,15 +43,15 @@
   fun merge data : T = Symtab.merge (op =) data handle Symtab.DUP name => err_dup name;
 );
 
-fun declare_keyword (name, kind) =
-  Data.map (fn data =>
-   (if is_none kind then Keyword.keyword name else ();
-    Symtab.update_new (name, Option.map Keyword.make kind) 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;
+    val _ = Keyword.declare name kind;
+  in Symtab.update_new (name, kind) data handle Symtab.DUP name => err_dup name end);
 
 fun the_keyword thy name =
   (case Symtab.lookup (Data.get thy) name of
-    SOME decl => decl
+    SOME kind => kind
   | NONE => error ("Unknown outer syntax keyword " ^ quote name));
 
 
diff -r 94aa7b81bcf6 -r d0181abdbdac src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/Pure/Thy/thy_output.ML	Thu Mar 15 22:08:53 2012 +0100
@@ -626,6 +626,8 @@
 
 (* embedded lemma *)
 
+val _ = Keyword.keyword "by";
+
 val _ =
   Context.>> (Context.map_theory
    (antiquotation (Binding.name "lemma")
diff -r 94aa7b81bcf6 -r d0181abdbdac src/Tools/Code_Generator.thy
--- a/src/Tools/Code_Generator.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/Tools/Code_Generator.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -6,7 +6,13 @@
 
 theory Code_Generator
 imports Pure
-keywords "datatypes" "functions" "module_name" "file" "checking"
+keywords
+  "try" "solve_direct" "quickcheck" "value" "print_codeproc"
+    "code_thms" "code_deps" "export_code" :: diag and
+  "quickcheck_params" "code_class" "code_instance" "code_type"
+    "code_const" "code_reserved" "code_include" "code_modulename"
+    "code_abort" "code_monad" "code_reflect" :: thy_decl and
+  "datatypes" "functions" "module_name" "file" "checking"
 uses
   "~~/src/Tools/misc_legacy.ML"
   "~~/src/Tools/cache_io.ML"
diff -r 94aa7b81bcf6 -r d0181abdbdac src/ZF/Datatype_ZF.thy
--- a/src/ZF/Datatype_ZF.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/ZF/Datatype_ZF.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -7,6 +7,7 @@
 
 theory Datatype_ZF
 imports Inductive_ZF Univ QUniv
+keywords "datatype" "codatatype" :: thy_decl
 uses "Tools/datatype_package.ML"
 begin
 
diff -r 94aa7b81bcf6 -r d0181abdbdac src/ZF/Inductive_ZF.thy
--- a/src/ZF/Inductive_ZF.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/ZF/Inductive_ZF.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -14,8 +14,10 @@
 theory Inductive_ZF
 imports Fixedpt QPair Nat_ZF
 keywords
+  "inductive" "coinductive" "rep_datatype" "primrec" :: thy_decl and
+  "inductive_cases" :: thy_script and
+  "domains" "intros" "monos" "con_defs" "type_intros" "type_elims"
   "elimination" "induction" "case_eqns" "recursor_eqns"
-  "domains" "intros" "monos" "con_defs" "type_intros" "type_elims"
 uses
   ("ind_syntax.ML")
   ("Tools/cartprod.ML")
diff -r 94aa7b81bcf6 -r d0181abdbdac src/ZF/upair.thy
--- a/src/ZF/upair.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/ZF/upair.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -11,8 +11,11 @@
 
 header{*Unordered Pairs*}
 
-theory upair imports ZF
-uses "Tools/typechk.ML" begin
+theory upair
+imports ZF
+keywords "print_tcset" :: diag
+uses "Tools/typechk.ML"
+begin
 
 setup TypeCheck.setup