1.1 --- a/src/HOL/HOLCF/Domain.thy	Thu Mar 15 17:45:54 2012 +0100
     1.2 +++ b/src/HOL/HOLCF/Domain.thy	Thu Mar 15 19:02:34 2012 +0100
     1.3 @@ -6,6 +6,7 @@
     1.4  
     1.5  theory Domain
     1.6  imports Representable Domain_Aux
     1.7 +keywords "lazy" "unsafe"
     1.8  uses
     1.9    ("Tools/domaindef.ML")
    1.10    ("Tools/Domain/domain_isomorphism.ML")

     2.1 --- a/src/HOL/HOLCF/Tools/Domain/domain.ML	Thu Mar 15 17:45:54 2012 +0100
     2.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain.ML	Thu Mar 15 19:02:34 2012 +0100
     2.3 @@ -228,9 +228,6 @@
     2.4  
     2.5  (** outer syntax **)
     2.6  
     2.7 -val _ = Keyword.keyword "lazy"
     2.8 -val _ = Keyword.keyword "unsafe"
     2.9 -
    2.10  val dest_decl : (bool * binding option * string) parser =
    2.11    Parse.$$$ "(" |-- Scan.optional (Parse.$$$ "lazy" >> K true) false --
    2.12      (Parse.binding >> SOME) -- (Parse.$$$ "::" |-- Parse.typ)  --| Parse.$$$ ")" >> Parse.triple1

     3.1 --- a/src/HOL/Import/Importer.thy	Thu Mar 15 17:45:54 2012 +0100
     3.2 +++ b/src/HOL/Import/Importer.thy	Thu Mar 15 19:02:34 2012 +0100
     3.3 @@ -4,6 +4,7 @@
     3.4  
     3.5  theory Importer
     3.6  imports Main
     3.7 +keywords ">"
     3.8  uses "shuffler.ML" "import_rews.ML" ("proof_kernel.ML") ("replay.ML") ("import.ML")
     3.9  begin
    3.10  

     4.1 --- a/src/HOL/Import/import.ML	Thu Mar 15 17:45:54 2012 +0100
     4.2 +++ b/src/HOL/Import/import.ML	Thu Mar 15 19:02:34 2012 +0100
     4.3 @@ -238,8 +238,7 @@
     4.4  val append_dump = (Parse.verbatim || Parse.string) >> add_dump
     4.5  
     4.6  val _ =
     4.7 -  (Keyword.keyword ">";
     4.8 -   Outer_Syntax.command "import_segment"
     4.9 +  (Outer_Syntax.command "import_segment"
    4.10                         "Set import segment name"
    4.11                         Keyword.thy_decl (import_segment >> Toplevel.theory);
    4.12     Outer_Syntax.command "import_theory"

     5.1 --- a/src/HOL/Inductive.thy	Thu Mar 15 17:45:54 2012 +0100
     5.2 +++ b/src/HOL/Inductive.thy	Thu Mar 15 19:02:34 2012 +0100
     5.3 @@ -6,6 +6,7 @@
     5.4  
     5.5  theory Inductive 
     5.6  imports Complete_Lattices
     5.7 +keywords "monos"
     5.8  uses
     5.9    "Tools/dseq.ML"
    5.10    ("Tools/inductive.ML")

     6.1 --- a/src/HOL/Library/Old_Recdef.thy	Thu Mar 15 17:45:54 2012 +0100
     6.2 +++ b/src/HOL/Library/Old_Recdef.thy	Thu Mar 15 19:02:34 2012 +0100
     6.3 @@ -6,7 +6,7 @@
     6.4  
     6.5  theory Old_Recdef
     6.6  imports Wfrec
     6.7 -keywords "recdef" :: thy_decl
     6.8 +keywords "recdef" :: thy_decl and "permissive" "congs" "hints"
     6.9  uses
    6.10    ("~~/src/HOL/Tools/TFL/casesplit.ML")
    6.11    ("~~/src/HOL/Tools/TFL/utils.ML")
    6.12 @@ -42,7 +42,7 @@
    6.13  lemma tfl_eq_True: "(x = True) --> x"
    6.14    by blast
    6.15  
    6.16 -lemma tfl_rev_eq_mp: "(x = y) --> y --> x";
    6.17 +lemma tfl_rev_eq_mp: "(x = y) --> y --> x"
    6.18    by blast
    6.19  
    6.20  lemma tfl_simp_thm: "(x --> y) --> (x = x') --> (x' --> y)"

     7.1 --- a/src/HOL/Nominal/Nominal.thy	Thu Mar 15 17:45:54 2012 +0100
     7.2 +++ b/src/HOL/Nominal/Nominal.thy	Thu Mar 15 19:02:34 2012 +0100
     7.3 @@ -1,5 +1,6 @@
     7.4  theory Nominal 
     7.5  imports Main "~~/src/HOL/Library/Infinite_Set"
     7.6 +keywords "avoids"
     7.7  uses
     7.8    ("nominal_thmdecls.ML")
     7.9    ("nominal_atoms.ML")

     8.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Thu Mar 15 17:45:54 2012 +0100
     8.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Mar 15 19:02:34 2012 +0100
     8.3 @@ -669,8 +669,6 @@
     8.4  
     8.5  (* outer syntax *)
     8.6  
     8.7 -val _ = Keyword.keyword "avoids";
     8.8 -
     8.9  val _ =
    8.10    Outer_Syntax.local_theory_to_proof "nominal_inductive"
    8.11      "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes"

     9.1 --- a/src/HOL/Quotient.thy	Thu Mar 15 17:45:54 2012 +0100
     9.2 +++ b/src/HOL/Quotient.thy	Thu Mar 15 19:02:34 2012 +0100
     9.3 @@ -6,6 +6,7 @@
     9.4  
     9.5  theory Quotient
     9.6  imports Plain Hilbert_Choice Equiv_Relations
     9.7 +keywords "/"
     9.8  uses
     9.9    ("Tools/Quotient/quotient_info.ML")
    9.10    ("Tools/Quotient/quotient_type.ML")

    10.1 --- a/src/HOL/Tools/Quotient/quotient_type.ML	Thu Mar 15 17:45:54 2012 +0100
    10.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML	Thu Mar 15 19:02:34 2012 +0100
    10.3 @@ -272,8 +272,6 @@
    10.4          (Parse.$$$ "/" |-- (partial -- Parse.term))  --
    10.5          Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding)))
    10.6  
    10.7 -val _ = Keyword.keyword "/"
    10.8 -
    10.9  val _ =
   10.10    Outer_Syntax.local_theory_to_proof "quotient_type"
   10.11      "quotient type definitions (require equivalence proofs)"

    11.1 --- a/src/HOL/Tools/inductive.ML	Thu Mar 15 17:45:54 2012 +0100
    11.2 +++ b/src/HOL/Tools/inductive.ML	Thu Mar 15 19:02:34 2012 +0100
    11.3 @@ -1134,8 +1134,6 @@
    11.4  
    11.5  (* outer syntax *)
    11.6  
    11.7 -val _ = Keyword.keyword "monos";
    11.8 -
    11.9  fun gen_ind_decl mk_def coind =
   11.10    Parse.fixes -- Parse.for_fixes --
   11.11    Scan.optional Parse_Spec.where_alt_specs [] --

    12.1 --- a/src/HOL/Tools/recdef.ML	Thu Mar 15 17:45:54 2012 +0100
    12.2 +++ b/src/HOL/Tools/recdef.ML	Thu Mar 15 19:02:34 2012 +0100
    12.3 @@ -290,8 +290,6 @@
    12.4  
    12.5  (* outer syntax *)
    12.6  
    12.7 -val _ = List.app Keyword.keyword ["permissive", "congs", "hints"];
    12.8 -
    12.9  val hints =
   12.10    Parse.$$$ "(" |--
   12.11      Parse.!!! (Parse.position (Parse.$$$ "hints" -- Args.parse) --| Parse.$$$ ")") >> Args.src;

    13.1 --- a/src/HOL/Tools/typedef.ML	Thu Mar 15 17:45:54 2012 +0100
    13.2 +++ b/src/HOL/Tools/typedef.ML	Thu Mar 15 19:02:34 2012 +0100
    13.3 @@ -299,8 +299,6 @@
    13.4  
    13.5  (** outer syntax **)
    13.6  
    13.7 -val _ = Keyword.keyword "morphisms";
    13.8 -
    13.9  val _ =
   13.10    Outer_Syntax.local_theory_to_proof "typedef" "HOL type definition (requires non-emptiness proof)"
   13.11      Keyword.thy_goal

    14.1 --- a/src/HOL/Typedef.thy	Thu Mar 15 17:45:54 2012 +0100
    14.2 +++ b/src/HOL/Typedef.thy	Thu Mar 15 19:02:34 2012 +0100
    14.3 @@ -6,6 +6,7 @@
    14.4  
    14.5  theory Typedef
    14.6  imports Set
    14.7 +keywords "morphisms"
    14.8  uses ("Tools/typedef.ML")
    14.9  begin
   14.10  

    15.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Mar 15 17:45:54 2012 +0100
    15.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Mar 15 19:02:34 2012 +0100
    15.3 @@ -12,15 +12,16 @@
    15.4  (*keep keywords consistent with the parsers, otherwise be prepared for
    15.5    unexpected errors*)
    15.6  
    15.7 -val _ = List.app Keyword.keyword
    15.8 - ["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
    15.9 -  "=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>",
   15.10 -  "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
   15.11 -  "advanced", "and", "assumes", "attach", "begin", "binder",
   15.12 -  "constrains", "defines", "fixes", "for", "identifier", "if",
   15.13 -  "imports", "in", "infix", "infixl", "infixr", "is", "keywords",
   15.14 -  "notes", "obtains", "open", "output", "overloaded", "pervasive",
   15.15 -  "shows", "structure", "unchecked", "uses", "where", "|"];
   15.16 +val _ = Context.>> (Context.map_theory
   15.17 +  (fold (fn name => Thy_Header.declare_keyword (name, NONE))
   15.18 +   ["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
   15.19 +    "=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>",
   15.20 +    "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
   15.21 +    "advanced", "and", "assumes", "attach", "begin", "binder",
   15.22 +    "constrains", "defines", "fixes", "for", "identifier", "if",
   15.23 +    "imports", "in", "infix", "infixl", "infixr", "is", "keywords",
   15.24 +    "notes", "obtains", "open", "output", "overloaded", "pervasive",
   15.25 +    "shows", "structure", "unchecked", "uses", "where", "|", "by"]));
   15.26  
   15.27  
   15.28  

    16.1 --- a/src/Pure/Thy/thy_header.ML	Thu Mar 15 17:45:54 2012 +0100
    16.2 +++ b/src/Pure/Thy/thy_header.ML	Thu Mar 15 19:02:34 2012 +0100
    16.3 @@ -45,8 +45,9 @@
    16.4  
    16.5  fun declare_keyword (name, kind) =
    16.6    Data.map (fn data =>
    16.7 +   (if is_none kind then Keyword.keyword name else ();
    16.8      Symtab.update_new (name, Option.map Keyword.make kind) data
    16.9 -      handle Symtab.DUP name => err_dup name);
   16.10 +      handle Symtab.DUP name => err_dup name));
   16.11  
   16.12  fun the_keyword thy name =
   16.13    (case Symtab.lookup (Data.get thy) name of

    17.1 --- a/src/Pure/Thy/thy_output.ML	Thu Mar 15 17:45:54 2012 +0100
    17.2 +++ b/src/Pure/Thy/thy_output.ML	Thu Mar 15 19:02:34 2012 +0100
    17.3 @@ -626,8 +626,6 @@
    17.4  
    17.5  (* embedded lemma *)
    17.6  
    17.7 -val _ = Keyword.keyword "by";
    17.8 -
    17.9  val _ =
   17.10    Context.>> (Context.map_theory
   17.11     (antiquotation (Binding.name "lemma")

    18.1 --- a/src/Tools/Code/code_printer.ML	Thu Mar 15 17:45:54 2012 +0100
    18.2 +++ b/src/Tools/Code/code_printer.ML	Thu Mar 15 19:02:34 2012 +0100
    18.3 @@ -405,8 +405,6 @@
    18.4          >> (fn ((x, i), s) => mk_complex (parse_infix prep_arg (x, i) s))
    18.5        || Parse.string >> (fn s => (parse_mixfix mk_plain mk_complex prep_arg s)));
    18.6  
    18.7 -val _ = List.app Keyword.keyword [infixK, infixlK, infixrK];
    18.8 -
    18.9  fun parse_tyco_syntax x = parse_syntax (fn s => (0, (K o K o K o str) s)) I I x;
   18.10  
   18.11  val parse_const_syntax = parse_syntax plain_const_syntax simple_const_syntax fst;

    19.1 --- a/src/Tools/Code/code_runtime.ML	Thu Mar 15 17:45:54 2012 +0100
    19.2 +++ b/src/Tools/Code/code_runtime.ML	Thu Mar 15 19:02:34 2012 +0100
    19.3 @@ -349,8 +349,6 @@
    19.4  val fileK = "file";
    19.5  val andK = "and"
    19.6  
    19.7 -val _ = List.app Keyword.keyword [datatypesK, functionsK];
    19.8 -
    19.9  val parse_datatype =
   19.10    Parse.name --| Parse.$$$ "=" --
   19.11      (((Parse.sym_ident || Parse.string) >> (fn "_" => NONE | _ => Scan.fail ()))

    20.1 --- a/src/Tools/Code/code_target.ML	Thu Mar 15 17:45:54 2012 +0100
    20.2 +++ b/src/Tools/Code/code_target.ML	Thu Mar 15 19:02:34 2012 +0100
    20.3 @@ -681,8 +681,6 @@
    20.4         -- Scan.optional (Parse.$$$ fileK |-- Parse.name) ""
    20.5         -- code_expr_argsP) >> (fn seris => export_code_cmd raw_cs seris)));
    20.6  
    20.7 -val _ = List.app Keyword.keyword [inK, module_nameK, fileK, checkingK];
    20.8 -
    20.9  val _ =
   20.10    Outer_Syntax.command "code_class" "define code syntax for class" Keyword.thy_decl (
   20.11      process_multi_syntax Parse.xname (Scan.option Parse.string)

    21.1 --- a/src/Tools/Code_Generator.thy	Thu Mar 15 17:45:54 2012 +0100
    21.2 +++ b/src/Tools/Code_Generator.thy	Thu Mar 15 19:02:34 2012 +0100
    21.3 @@ -6,6 +6,7 @@
    21.4  
    21.5  theory Code_Generator
    21.6  imports Pure
    21.7 +keywords "datatypes" "functions" "module_name" "file" "checking"
    21.8  uses
    21.9    "~~/src/Tools/misc_legacy.ML"
   21.10    "~~/src/Tools/cache_io.ML"

    22.1 --- a/src/Tools/interpretation_with_defs.ML	Thu Mar 15 17:45:54 2012 +0100
    22.2 +++ b/src/Tools/interpretation_with_defs.ML	Thu Mar 15 19:02:34 2012 +0100
    22.3 @@ -79,14 +79,11 @@
    22.4  
    22.5  end;
    22.6  
    22.7 -val definesK = "defines";
    22.8 -val _ = Keyword.keyword definesK;
    22.9 -
   22.10  val _ =
   22.11    Outer_Syntax.command "interpretation"
   22.12      "prove interpretation of locale expression in theory" Keyword.thy_goal
   22.13      (Parse.!!! (Parse_Spec.locale_expression true) --
   22.14 -      Scan.optional (Parse.$$$ definesK |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
   22.15 +      Scan.optional (Parse.$$$ "defines" |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
   22.16          -- ((Parse.binding -- Parse.opt_mixfix') --| Parse.$$$ "is" -- Parse.term))) [] --
   22.17        Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
   22.18        >> (fn ((expr, defs), equations) => Toplevel.print o

    23.1 --- a/src/ZF/Inductive_ZF.thy	Thu Mar 15 17:45:54 2012 +0100
    23.2 +++ b/src/ZF/Inductive_ZF.thy	Thu Mar 15 19:02:34 2012 +0100
    23.3 @@ -13,6 +13,9 @@
    23.4  
    23.5  theory Inductive_ZF
    23.6  imports Fixedpt QPair Nat_ZF
    23.7 +keywords
    23.8 +  "elimination" "induction" "case_eqns" "recursor_eqns"
    23.9 +  "domains" "intros" "monos" "con_defs" "type_intros" "type_elims"
   23.10  uses
   23.11    ("ind_syntax.ML")
   23.12    ("Tools/cartprod.ML")

    24.1 --- a/src/ZF/Tools/induct_tacs.ML	Thu Mar 15 17:45:54 2012 +0100
    24.2 +++ b/src/ZF/Tools/induct_tacs.ML	Thu Mar 15 19:02:34 2012 +0100
    24.3 @@ -188,8 +188,6 @@
    24.4  
    24.5  (* outer syntax *)
    24.6  
    24.7 -val _ = List.app Keyword.keyword ["elimination", "induction", "case_eqns", "recursor_eqns"];
    24.8 -
    24.9  val rep_datatype_decl =
   24.10    (Parse.$$$ "elimination" |-- Parse.!!! Parse_Spec.xthm) --
   24.11    (Parse.$$$ "induction" |-- Parse.!!! Parse_Spec.xthm) --

    25.1 --- a/src/ZF/Tools/inductive_package.ML	Thu Mar 15 17:45:54 2012 +0100
    25.2 +++ b/src/ZF/Tools/inductive_package.ML	Thu Mar 15 19:02:34 2012 +0100
    25.3 @@ -576,9 +576,6 @@
    25.4  
    25.5  (* outer syntax *)
    25.6  
    25.7 -val _ = List.app Keyword.keyword
    25.8 -  ["domains", "intros", "monos", "con_defs", "type_intros", "type_elims"];
    25.9 -
   25.10  fun mk_ind (((((doms, intrs), monos), con_defs), type_intrs), type_elims) =
   25.11    #1 o add_inductive doms (map Parse.triple_swap intrs) (monos, con_defs, type_intrs, type_elims);
   25.12