--- 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 *)
--- 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 --
--- 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;
--- 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.$$$ ")") "" --
--- 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;
--- 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 --
--- 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;
--- 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 =
--- 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
--- 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;
--- 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
--- 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 --
--- 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;
--- 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 =
--- 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)))));
--- 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.$$$ ")") [];
--- 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
--- 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";
--- 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
--- 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);
--- 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)
--- 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) --
--- 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);
--- 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);
--- 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)))));