# HG changeset patch
# User wenzelm
# Date 1124192546 -7200
# Node ID 0934ac31985fd994faa3969fc154eab125020aa6
# Parent  05fc32a23b8b2443261e3c62b33a4407c42e3664
OuterKeyword;

diff -r 05fc32a23b8b -r 0934ac31985f src/HOL/Import/import_syntax.ML
--- a/src/HOL/Import/import_syntax.ML	Tue Aug 16 13:42:23 2005 +0200
+++ b/src/HOL/Import/import_syntax.ML	Tue Aug 16 13:42:26 2005 +0200
@@ -30,7 +30,7 @@
 
 type token = OuterSyntax.token
 
-local structure P = OuterParse and K = OuterSyntax.Keyword in
+local structure P = OuterParse and K = OuterKeyword in
 
 (* Parsers *)
 
diff -r 05fc32a23b8b -r 0934ac31985f src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Tue Aug 16 13:42:23 2005 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Tue Aug 16 13:42:26 2005 +0200
@@ -954,7 +954,7 @@
 
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterSyntax.Keyword in
+local structure P = OuterParse and K = OuterKeyword in
 
 val datatype_decl =
   Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --
diff -r 05fc32a23b8b -r 0934ac31985f src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Tue Aug 16 13:42:23 2005 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Tue Aug 16 13:42:26 2005 +0200
@@ -878,7 +878,7 @@
 
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterSyntax.Keyword in
+local structure P = OuterParse and K = OuterKeyword in
 
 fun mk_ind coind ((sets, intrs), monos) =
   #1 o add_inductive true coind sets (map P.triple_swap intrs) monos;
diff -r 05fc32a23b8b -r 0934ac31985f src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Tue Aug 16 13:42:23 2005 +0200
+++ b/src/HOL/Tools/primrec_package.ML	Tue Aug 16 13:42:26 2005 +0200
@@ -286,7 +286,7 @@
 
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterSyntax.Keyword in
+local structure P = OuterParse and K = OuterKeyword in
 
 val primrec_decl =
   Scan.optional (P.$$$ "(" |-- P.name --| P.$$$ ")") "" --
diff -r 05fc32a23b8b -r 0934ac31985f src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Tue Aug 16 13:42:23 2005 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Tue Aug 16 13:42:26 2005 +0200
@@ -338,7 +338,7 @@
 
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterSyntax.Keyword in
+local structure P = OuterParse and K = OuterKeyword in
 
 val hints =
   P.$$$ "(" |-- P.!!! (P.position (P.$$$ "hints" -- P.arguments) --| P.$$$ ")") >> Args.src;
diff -r 05fc32a23b8b -r 0934ac31985f src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Tue Aug 16 13:42:23 2005 +0200
+++ b/src/HOL/Tools/record_package.ML	Tue Aug 16 13:42:26 2005 +0200
@@ -2131,7 +2131,7 @@
 
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterSyntax.Keyword in
+local structure P = OuterParse and K = OuterKeyword in
 
 val record_decl =
   P.type_args -- P.name --
diff -r 05fc32a23b8b -r 0934ac31985f src/HOL/Tools/refute_isar.ML
--- a/src/HOL/Tools/refute_isar.ML	Tue Aug 16 13:42:23 2005 +0200
+++ b/src/HOL/Tools/refute_isar.ML	Tue Aug 16 13:42:26 2005 +0200
@@ -54,7 +54,7 @@
 
 	fun refute_parser tokens = (refute_scan_args tokens) |>> refute_trans;
 
-	val refute_cmd = OuterSyntax.improper_command "refute" "try to find a model that refutes a given subgoal" OuterSyntax.Keyword.diag refute_parser;
+	val refute_cmd = OuterSyntax.improper_command "refute" "try to find a model that refutes a given subgoal" OuterKeyword.diag refute_parser;
 
 (* ------------------------------------------------------------------------- *)
 (* set up the 'refute_params' command                                        *)
@@ -90,7 +90,7 @@
 
 	fun refute_params_parser tokens = (refute_params_scan_args tokens) |>> refute_params_trans;
 
-	val refute_params_cmd = OuterSyntax.command "refute_params" "show/store default parameters for the 'refute' command" OuterSyntax.Keyword.thy_decl refute_params_parser;
+	val refute_params_cmd = OuterSyntax.command "refute_params" "show/store default parameters for the 'refute' command" OuterKeyword.thy_decl refute_params_parser;
 
 end;
 
diff -r 05fc32a23b8b -r 0934ac31985f src/HOL/Tools/specification_package.ML
--- a/src/HOL/Tools/specification_package.ML	Tue Aug 16 13:42:23 2005 +0200
+++ b/src/HOL/Tools/specification_package.ML	Tue Aug 16 13:42:26 2005 +0200
@@ -239,7 +239,7 @@
 
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterSyntax.Keyword in
+local structure P = OuterParse and K = OuterKeyword in
 
 (* taken from ~~/Pure/Isar/isar_syn.ML *)
 val opt_overloaded =
diff -r 05fc32a23b8b -r 0934ac31985f src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Tue Aug 16 13:42:23 2005 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Tue Aug 16 13:42:26 2005 +0200
@@ -364,7 +364,7 @@
 
 (** outer syntax **)
 
-local structure P = OuterParse and K = OuterSyntax.Keyword in
+local structure P = OuterParse and K = OuterKeyword in
 
 val typedeclP =
   OuterSyntax.command "typedecl" "type declaration (HOL)" K.thy_decl
diff -r 05fc32a23b8b -r 0934ac31985f src/HOLCF/IOA/meta_theory/ioa_package.ML
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Tue Aug 16 13:42:23 2005 +0200
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Tue Aug 16 13:42:26 2005 +0200
@@ -489,7 +489,7 @@
 
 (* parsers *)
 
-local structure P = OuterParse and K = OuterSyntax.Keyword in
+local structure P = OuterParse and K = OuterKeyword in
 
 val actionlist = P.list1 P.term;
 val inputslist = P.$$$ "inputs" |-- actionlist;
diff -r 05fc32a23b8b -r 0934ac31985f src/HOLCF/cont_consts.ML
--- a/src/HOLCF/cont_consts.ML	Tue Aug 16 13:42:23 2005 +0200
+++ b/src/HOLCF/cont_consts.ML	Tue Aug 16 13:42:26 2005 +0200
@@ -97,7 +97,7 @@
 
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterSyntax.Keyword in
+local structure P = OuterParse and K = OuterKeyword in
 
 val constsP =
   OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl
diff -r 05fc32a23b8b -r 0934ac31985f src/HOLCF/domain/extender.ML
--- a/src/HOLCF/domain/extender.ML	Tue Aug 16 13:42:23 2005 +0200
+++ b/src/HOLCF/domain/extender.ML	Tue Aug 16 13:42:26 2005 +0200
@@ -140,7 +140,7 @@
 
 (** outer syntax **)
 
-local structure P = OuterParse and K = OuterSyntax.Keyword in
+local structure P = OuterParse and K = OuterKeyword in
 
 val dest_decl =
   P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
diff -r 05fc32a23b8b -r 0934ac31985f src/HOLCF/fixrec_package.ML
--- a/src/HOLCF/fixrec_package.ML	Tue Aug 16 13:42:23 2005 +0200
+++ b/src/HOLCF/fixrec_package.ML	Tue Aug 16 13:42:26 2005 +0200
@@ -296,7 +296,7 @@
 (******************************** Parsers ********************************)
 (*************************************************************************)
 
-local structure P = OuterParse and K = OuterSyntax.Keyword in
+local structure P = OuterParse and K = OuterKeyword in
 
 val fixrec_eqn = P.opt_thm_name ":" -- P.prop;
 
diff -r 05fc32a23b8b -r 0934ac31985f src/HOLCF/pcpodef_package.ML
--- a/src/HOLCF/pcpodef_package.ML	Tue Aug 16 13:42:23 2005 +0200
+++ b/src/HOLCF/pcpodef_package.ML	Tue Aug 16 13:42:26 2005 +0200
@@ -185,7 +185,7 @@
 
 (** outer syntax **)
 
-local structure P = OuterParse and K = OuterSyntax.Keyword in
+local structure P = OuterParse and K = OuterKeyword in
 
 (* copied from HOL/Tools/typedef_package.ML *)
 val typedef_proof_decl =
diff -r 05fc32a23b8b -r 0934ac31985f src/Provers/classical.ML
--- a/src/Provers/classical.ML	Tue Aug 16 13:42:23 2005 +0200
+++ b/src/Provers/classical.ML	Tue Aug 16 13:42:26 2005 +0200
@@ -1062,7 +1062,7 @@
 
 val print_clasetP =
   OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner"
-    OuterSyntax.Keyword.diag
+    OuterKeyword.diag
     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep
       (Toplevel.node_case print_claset (print_local_claset o Proof.context_of)))));
 
diff -r 05fc32a23b8b -r 0934ac31985f src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Tue Aug 16 13:42:23 2005 +0200
+++ b/src/Pure/Proof/extraction.ML	Tue Aug 16 13:42:26 2005 +0200
@@ -761,7 +761,7 @@
 
 (**** interface ****)
 
-structure P = OuterParse and K = OuterSyntax.Keyword;
+structure P = OuterParse and K = OuterKeyword;
 
 val parse_vars = Scan.optional (P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") [];
 
diff -r 05fc32a23b8b -r 0934ac31985f src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Tue Aug 16 13:42:23 2005 +0200
+++ b/src/Pure/axclass.ML	Tue Aug 16 13:42:26 2005 +0200
@@ -362,7 +362,7 @@
 
 (** outer syntax **)
 
-local structure P = OuterParse and K = OuterSyntax.Keyword in
+local structure P = OuterParse and K = OuterKeyword in
 
 val axclassP =
   OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
diff -r 05fc32a23b8b -r 0934ac31985f src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Tue Aug 16 13:42:23 2005 +0200
+++ b/src/Pure/codegen.ML	Tue Aug 16 13:42:26 2005 +0200
@@ -896,7 +896,7 @@
        \  in (fn x => !f x) end;\n")]))]];
 
 
-structure P = OuterParse and K = OuterSyntax.Keyword;
+structure P = OuterParse and K = OuterKeyword;
 
 fun strip_newlines s = implode (fst (take_suffix (equal "\n")
   (snd (take_prefix (equal "\n") (explode s))))) ^ "\n";
diff -r 05fc32a23b8b -r 0934ac31985f src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Tue Aug 16 13:42:23 2005 +0200
+++ b/src/Pure/proof_general.ML	Tue Aug 16 13:42:26 2005 +0200
@@ -1369,7 +1369,7 @@
 
 (* additional outer syntax for Isar *)
 
-local structure P = OuterParse and K = OuterSyntax.Keyword in
+local structure P = OuterParse and K = OuterKeyword in
 
 val undoP = (*undo without output*)
   OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
@@ -1483,7 +1483,7 @@
   \;;\n" ^
   defconst "major" (map #1 commands) ^
   defconst "minor" (List.filter Syntax.is_identifier keywords) ^
-  implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^
+  implode (map (make_elisp_commands commands) OuterKeyword.kinds) ^
   "\n(provide 'isar-keywords)\n";
 
 in
diff -r 05fc32a23b8b -r 0934ac31985f src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Tue Aug 16 13:42:23 2005 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Tue Aug 16 13:42:26 2005 +0200
@@ -418,7 +418,7 @@
 
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterSyntax.Keyword in
+local structure P = OuterParse and K = OuterKeyword in
 
 fun mk_datatype ((((dom, dts), monos), type_intrs), type_elims) =
   #1 o add_datatype (dom, map fst dts) (map snd dts) (monos, type_intrs, type_elims);
diff -r 05fc32a23b8b -r 0934ac31985f src/ZF/Tools/ind_cases.ML
--- a/src/ZF/Tools/ind_cases.ML	Tue Aug 16 13:42:23 2005 +0200
+++ b/src/ZF/Tools/ind_cases.ML	Tue Aug 16 13:42:26 2005 +0200
@@ -79,7 +79,7 @@
 
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterSyntax.Keyword in
+local structure P = OuterParse and K = OuterKeyword in
 
 val ind_cases =
   P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop)
diff -r 05fc32a23b8b -r 0934ac31985f src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Tue Aug 16 13:42:23 2005 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Tue Aug 16 13:42:26 2005 +0200
@@ -200,7 +200,7 @@
 
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterSyntax.Keyword in
+local structure P = OuterParse and K = OuterKeyword in
 
 val rep_datatype_decl =
   (P.$$$ "elimination" |-- P.!!! P.xthm) --
diff -r 05fc32a23b8b -r 0934ac31985f src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Tue Aug 16 13:42:23 2005 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Tue Aug 16 13:42:26 2005 +0200
@@ -596,7 +596,7 @@
 
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterSyntax.Keyword in
+local structure P = OuterParse and K = OuterKeyword in
 
 fun mk_ind (((((doms, intrs), monos), con_defs), type_intrs), type_elims) =
   #1 o add_inductive doms (map P.triple_swap intrs) (monos, con_defs, type_intrs, type_elims);
diff -r 05fc32a23b8b -r 0934ac31985f src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Tue Aug 16 13:42:23 2005 +0200
+++ b/src/ZF/Tools/primrec_package.ML	Tue Aug 16 13:42:26 2005 +0200
@@ -200,7 +200,7 @@
 
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterSyntax.Keyword in
+local structure P = OuterParse and K = OuterKeyword in
 
 val primrec_decl = Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
 
diff -r 05fc32a23b8b -r 0934ac31985f src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Tue Aug 16 13:42:23 2005 +0200
+++ b/src/ZF/Tools/typechk.ML	Tue Aug 16 13:42:26 2005 +0200
@@ -220,7 +220,7 @@
 
 val print_tcsetP =
   OuterSyntax.improper_command "print_tcset" "print context of ZF type-checker"
-    OuterSyntax.Keyword.diag
+    OuterKeyword.diag
     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep
       (Toplevel.node_case print_tcset (LocalTypecheckingData.print o Proof.context_of)))));