--- 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")
--- 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
--- 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
--- 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"
--- 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")
--- 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)"
--- 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")
--- 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"
--- 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")
--- 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)"
--- 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 [] --
--- 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;
--- 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
--- 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
--- 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"]));
--- 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
--- 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")
--- 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;
--- 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 ()))
--- 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)
--- 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"
--- 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
--- 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")
--- 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) --
--- 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);