# HG changeset patch
# User wenzelm
# Date 1331834554 -3600
# Node ID b8c7eb0c2f89fa6d1b43509ba1348dd8301fa393
# Parent  acc8ebf980cae9a8774bff19fbb8cbe53f092e79
declare minor keywords via theory header;

diff -r acc8ebf980ca -r b8c7eb0c2f89 src/HOL/HOLCF/Domain.thy
--- a/src/HOL/HOLCF/Domain.thy	Thu Mar 15 17:45:54 2012 +0100
+++ b/src/HOL/HOLCF/Domain.thy	Thu Mar 15 19:02:34 2012 +0100
@@ -6,6 +6,7 @@
 
 theory Domain
 imports Representable Domain_Aux
+keywords "lazy" "unsafe"
 uses
   ("Tools/domaindef.ML")
   ("Tools/Domain/domain_isomorphism.ML")
diff -r acc8ebf980ca -r b8c7eb0c2f89 src/HOL/HOLCF/Tools/Domain/domain.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain.ML	Thu Mar 15 17:45:54 2012 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain.ML	Thu Mar 15 19:02:34 2012 +0100
@@ -228,9 +228,6 @@
 
 (** outer syntax **)
 
-val _ = Keyword.keyword "lazy"
-val _ = Keyword.keyword "unsafe"
-
 val dest_decl : (bool * binding option * string) parser =
   Parse.$$$ "(" |-- Scan.optional (Parse.$$$ "lazy" >> K true) false --
     (Parse.binding >> SOME) -- (Parse.$$$ "::" |-- Parse.typ)  --| Parse.$$$ ")" >> Parse.triple1
diff -r acc8ebf980ca -r b8c7eb0c2f89 src/HOL/Import/Importer.thy
--- a/src/HOL/Import/Importer.thy	Thu Mar 15 17:45:54 2012 +0100
+++ b/src/HOL/Import/Importer.thy	Thu Mar 15 19:02:34 2012 +0100
@@ -4,6 +4,7 @@
 
 theory Importer
 imports Main
+keywords ">"
 uses "shuffler.ML" "import_rews.ML" ("proof_kernel.ML") ("replay.ML") ("import.ML")
 begin
 
diff -r acc8ebf980ca -r b8c7eb0c2f89 src/HOL/Import/import.ML
--- a/src/HOL/Import/import.ML	Thu Mar 15 17:45:54 2012 +0100
+++ b/src/HOL/Import/import.ML	Thu Mar 15 19:02:34 2012 +0100
@@ -238,8 +238,7 @@
 val append_dump = (Parse.verbatim || Parse.string) >> add_dump
 
 val _ =
-  (Keyword.keyword ">";
-   Outer_Syntax.command "import_segment"
+  (Outer_Syntax.command "import_segment"
                        "Set import segment name"
                        Keyword.thy_decl (import_segment >> Toplevel.theory);
    Outer_Syntax.command "import_theory"
diff -r acc8ebf980ca -r b8c7eb0c2f89 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Thu Mar 15 17:45:54 2012 +0100
+++ b/src/HOL/Inductive.thy	Thu Mar 15 19:02:34 2012 +0100
@@ -6,6 +6,7 @@
 
 theory Inductive 
 imports Complete_Lattices
+keywords "monos"
 uses
   "Tools/dseq.ML"
   ("Tools/inductive.ML")
diff -r acc8ebf980ca -r b8c7eb0c2f89 src/HOL/Library/Old_Recdef.thy
--- a/src/HOL/Library/Old_Recdef.thy	Thu Mar 15 17:45:54 2012 +0100
+++ b/src/HOL/Library/Old_Recdef.thy	Thu Mar 15 19:02:34 2012 +0100
@@ -6,7 +6,7 @@
 
 theory Old_Recdef
 imports Wfrec
-keywords "recdef" :: thy_decl
+keywords "recdef" :: thy_decl and "permissive" "congs" "hints"
 uses
   ("~~/src/HOL/Tools/TFL/casesplit.ML")
   ("~~/src/HOL/Tools/TFL/utils.ML")
@@ -42,7 +42,7 @@
 lemma tfl_eq_True: "(x = True) --> x"
   by blast
 
-lemma tfl_rev_eq_mp: "(x = y) --> y --> x";
+lemma tfl_rev_eq_mp: "(x = y) --> y --> x"
   by blast
 
 lemma tfl_simp_thm: "(x --> y) --> (x = x') --> (x' --> y)"
diff -r acc8ebf980ca -r b8c7eb0c2f89 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Thu Mar 15 17:45:54 2012 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Thu Mar 15 19:02:34 2012 +0100
@@ -1,5 +1,6 @@
 theory Nominal 
 imports Main "~~/src/HOL/Library/Infinite_Set"
+keywords "avoids"
 uses
   ("nominal_thmdecls.ML")
   ("nominal_atoms.ML")
diff -r acc8ebf980ca -r b8c7eb0c2f89 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Thu Mar 15 17:45:54 2012 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Mar 15 19:02:34 2012 +0100
@@ -669,8 +669,6 @@
 
 (* outer syntax *)
 
-val _ = Keyword.keyword "avoids";
-
 val _ =
   Outer_Syntax.local_theory_to_proof "nominal_inductive"
     "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes"
diff -r acc8ebf980ca -r b8c7eb0c2f89 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Thu Mar 15 17:45:54 2012 +0100
+++ b/src/HOL/Quotient.thy	Thu Mar 15 19:02:34 2012 +0100
@@ -6,6 +6,7 @@
 
 theory Quotient
 imports Plain Hilbert_Choice Equiv_Relations
+keywords "/"
 uses
   ("Tools/Quotient/quotient_info.ML")
   ("Tools/Quotient/quotient_type.ML")
diff -r acc8ebf980ca -r b8c7eb0c2f89 src/HOL/Tools/Quotient/quotient_type.ML
--- a/src/HOL/Tools/Quotient/quotient_type.ML	Thu Mar 15 17:45:54 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_type.ML	Thu Mar 15 19:02:34 2012 +0100
@@ -272,8 +272,6 @@
         (Parse.$$$ "/" |-- (partial -- Parse.term))  --
         Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding)))
 
-val _ = Keyword.keyword "/"
-
 val _ =
   Outer_Syntax.local_theory_to_proof "quotient_type"
     "quotient type definitions (require equivalence proofs)"
diff -r acc8ebf980ca -r b8c7eb0c2f89 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Thu Mar 15 17:45:54 2012 +0100
+++ b/src/HOL/Tools/inductive.ML	Thu Mar 15 19:02:34 2012 +0100
@@ -1134,8 +1134,6 @@
 
 (* outer syntax *)
 
-val _ = Keyword.keyword "monos";
-
 fun gen_ind_decl mk_def coind =
   Parse.fixes -- Parse.for_fixes --
   Scan.optional Parse_Spec.where_alt_specs [] --
diff -r acc8ebf980ca -r b8c7eb0c2f89 src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Thu Mar 15 17:45:54 2012 +0100
+++ b/src/HOL/Tools/recdef.ML	Thu Mar 15 19:02:34 2012 +0100
@@ -290,8 +290,6 @@
 
 (* outer syntax *)
 
-val _ = List.app Keyword.keyword ["permissive", "congs", "hints"];
-
 val hints =
   Parse.$$$ "(" |--
     Parse.!!! (Parse.position (Parse.$$$ "hints" -- Args.parse) --| Parse.$$$ ")") >> Args.src;
diff -r acc8ebf980ca -r b8c7eb0c2f89 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Thu Mar 15 17:45:54 2012 +0100
+++ b/src/HOL/Tools/typedef.ML	Thu Mar 15 19:02:34 2012 +0100
@@ -299,8 +299,6 @@
 
 (** outer syntax **)
 
-val _ = Keyword.keyword "morphisms";
-
 val _ =
   Outer_Syntax.local_theory_to_proof "typedef" "HOL type definition (requires non-emptiness proof)"
     Keyword.thy_goal
diff -r acc8ebf980ca -r b8c7eb0c2f89 src/HOL/Typedef.thy
--- a/src/HOL/Typedef.thy	Thu Mar 15 17:45:54 2012 +0100
+++ b/src/HOL/Typedef.thy	Thu Mar 15 19:02:34 2012 +0100
@@ -6,6 +6,7 @@
 
 theory Typedef
 imports Set
+keywords "morphisms"
 uses ("Tools/typedef.ML")
 begin
 
diff -r acc8ebf980ca -r b8c7eb0c2f89 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Mar 15 17:45:54 2012 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Mar 15 19:02:34 2012 +0100
@@ -12,15 +12,16 @@
 (*keep keywords consistent with the parsers, otherwise be prepared for
   unexpected errors*)
 
-val _ = List.app Keyword.keyword
- ["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
-  "=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>",
-  "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
-  "advanced", "and", "assumes", "attach", "begin", "binder",
-  "constrains", "defines", "fixes", "for", "identifier", "if",
-  "imports", "in", "infix", "infixl", "infixr", "is", "keywords",
-  "notes", "obtains", "open", "output", "overloaded", "pervasive",
-  "shows", "structure", "unchecked", "uses", "where", "|"];
+val _ = Context.>> (Context.map_theory
+  (fold (fn name => Thy_Header.declare_keyword (name, NONE))
+   ["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
+    "=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>",
+    "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
+    "advanced", "and", "assumes", "attach", "begin", "binder",
+    "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"]));
 
 
 
diff -r acc8ebf980ca -r b8c7eb0c2f89 src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Thu Mar 15 17:45:54 2012 +0100
+++ b/src/Pure/Thy/thy_header.ML	Thu Mar 15 19:02:34 2012 +0100
@@ -45,8 +45,9 @@
 
 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);
+      handle Symtab.DUP name => err_dup name));
 
 fun the_keyword thy name =
   (case Symtab.lookup (Data.get thy) name of
diff -r acc8ebf980ca -r b8c7eb0c2f89 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Thu Mar 15 17:45:54 2012 +0100
+++ b/src/Pure/Thy/thy_output.ML	Thu Mar 15 19:02:34 2012 +0100
@@ -626,8 +626,6 @@
 
 (* embedded lemma *)
 
-val _ = Keyword.keyword "by";
-
 val _ =
   Context.>> (Context.map_theory
    (antiquotation (Binding.name "lemma")
diff -r acc8ebf980ca -r b8c7eb0c2f89 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Thu Mar 15 17:45:54 2012 +0100
+++ b/src/Tools/Code/code_printer.ML	Thu Mar 15 19:02:34 2012 +0100
@@ -405,8 +405,6 @@
         >> (fn ((x, i), s) => mk_complex (parse_infix prep_arg (x, i) s))
       || Parse.string >> (fn s => (parse_mixfix mk_plain mk_complex prep_arg s)));
 
-val _ = List.app Keyword.keyword [infixK, infixlK, infixrK];
-
 fun parse_tyco_syntax x = parse_syntax (fn s => (0, (K o K o K o str) s)) I I x;
 
 val parse_const_syntax = parse_syntax plain_const_syntax simple_const_syntax fst;
diff -r acc8ebf980ca -r b8c7eb0c2f89 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Thu Mar 15 17:45:54 2012 +0100
+++ b/src/Tools/Code/code_runtime.ML	Thu Mar 15 19:02:34 2012 +0100
@@ -349,8 +349,6 @@
 val fileK = "file";
 val andK = "and"
 
-val _ = List.app Keyword.keyword [datatypesK, functionsK];
-
 val parse_datatype =
   Parse.name --| Parse.$$$ "=" --
     (((Parse.sym_ident || Parse.string) >> (fn "_" => NONE | _ => Scan.fail ()))
diff -r acc8ebf980ca -r b8c7eb0c2f89 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Thu Mar 15 17:45:54 2012 +0100
+++ b/src/Tools/Code/code_target.ML	Thu Mar 15 19:02:34 2012 +0100
@@ -681,8 +681,6 @@
        -- Scan.optional (Parse.$$$ fileK |-- Parse.name) ""
        -- code_expr_argsP) >> (fn seris => export_code_cmd raw_cs seris)));
 
-val _ = List.app Keyword.keyword [inK, module_nameK, fileK, checkingK];
-
 val _ =
   Outer_Syntax.command "code_class" "define code syntax for class" Keyword.thy_decl (
     process_multi_syntax Parse.xname (Scan.option Parse.string)
diff -r acc8ebf980ca -r b8c7eb0c2f89 src/Tools/Code_Generator.thy
--- a/src/Tools/Code_Generator.thy	Thu Mar 15 17:45:54 2012 +0100
+++ b/src/Tools/Code_Generator.thy	Thu Mar 15 19:02:34 2012 +0100
@@ -6,6 +6,7 @@
 
 theory Code_Generator
 imports Pure
+keywords "datatypes" "functions" "module_name" "file" "checking"
 uses
   "~~/src/Tools/misc_legacy.ML"
   "~~/src/Tools/cache_io.ML"
diff -r acc8ebf980ca -r b8c7eb0c2f89 src/Tools/interpretation_with_defs.ML
--- a/src/Tools/interpretation_with_defs.ML	Thu Mar 15 17:45:54 2012 +0100
+++ b/src/Tools/interpretation_with_defs.ML	Thu Mar 15 19:02:34 2012 +0100
@@ -79,14 +79,11 @@
 
 end;
 
-val definesK = "defines";
-val _ = Keyword.keyword definesK;
-
 val _ =
   Outer_Syntax.command "interpretation"
     "prove interpretation of locale expression in theory" Keyword.thy_goal
     (Parse.!!! (Parse_Spec.locale_expression true) --
-      Scan.optional (Parse.$$$ definesK |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
+      Scan.optional (Parse.$$$ "defines" |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
         -- ((Parse.binding -- Parse.opt_mixfix') --| Parse.$$$ "is" -- Parse.term))) [] --
       Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
       >> (fn ((expr, defs), equations) => Toplevel.print o
diff -r acc8ebf980ca -r b8c7eb0c2f89 src/ZF/Inductive_ZF.thy
--- a/src/ZF/Inductive_ZF.thy	Thu Mar 15 17:45:54 2012 +0100
+++ b/src/ZF/Inductive_ZF.thy	Thu Mar 15 19:02:34 2012 +0100
@@ -13,6 +13,9 @@
 
 theory Inductive_ZF
 imports Fixedpt QPair Nat_ZF
+keywords
+  "elimination" "induction" "case_eqns" "recursor_eqns"
+  "domains" "intros" "monos" "con_defs" "type_intros" "type_elims"
 uses
   ("ind_syntax.ML")
   ("Tools/cartprod.ML")
diff -r acc8ebf980ca -r b8c7eb0c2f89 src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Thu Mar 15 17:45:54 2012 +0100
+++ b/src/ZF/Tools/induct_tacs.ML	Thu Mar 15 19:02:34 2012 +0100
@@ -188,8 +188,6 @@
 
 (* outer syntax *)
 
-val _ = List.app Keyword.keyword ["elimination", "induction", "case_eqns", "recursor_eqns"];
-
 val rep_datatype_decl =
   (Parse.$$$ "elimination" |-- Parse.!!! Parse_Spec.xthm) --
   (Parse.$$$ "induction" |-- Parse.!!! Parse_Spec.xthm) --
diff -r acc8ebf980ca -r b8c7eb0c2f89 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Thu Mar 15 17:45:54 2012 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Thu Mar 15 19:02:34 2012 +0100
@@ -576,9 +576,6 @@
 
 (* outer syntax *)
 
-val _ = List.app Keyword.keyword
-  ["domains", "intros", "monos", "con_defs", "type_intros", "type_elims"];
-
 fun mk_ind (((((doms, intrs), monos), con_defs), type_intrs), type_elims) =
   #1 o add_inductive doms (map Parse.triple_swap intrs) (monos, con_defs, type_intrs, type_elims);