OuterKeyword;
authorwenzelm
Tue Aug 16 13:42:26 2005 +0200 (2005-08-16)
changeset 170570934ac31985f
parent 17056 05fc32a23b8b
child 17058 a5737356d806
OuterKeyword;
src/HOL/Import/import_syntax.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/recdef_package.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/refute_isar.ML
src/HOL/Tools/specification_package.ML
src/HOL/Tools/typedef_package.ML
src/HOLCF/IOA/meta_theory/ioa_package.ML
src/HOLCF/cont_consts.ML
src/HOLCF/domain/extender.ML
src/HOLCF/fixrec_package.ML
src/HOLCF/pcpodef_package.ML
src/Provers/classical.ML
src/Pure/Proof/extraction.ML
src/Pure/axclass.ML
src/Pure/codegen.ML
src/Pure/proof_general.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/ind_cases.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/primrec_package.ML
src/ZF/Tools/typechk.ML
     1.1 --- a/src/HOL/Import/import_syntax.ML	Tue Aug 16 13:42:23 2005 +0200
     1.2 +++ b/src/HOL/Import/import_syntax.ML	Tue Aug 16 13:42:26 2005 +0200
     1.3 @@ -30,7 +30,7 @@
     1.4  
     1.5  type token = OuterSyntax.token
     1.6  
     1.7 -local structure P = OuterParse and K = OuterSyntax.Keyword in
     1.8 +local structure P = OuterParse and K = OuterKeyword in
     1.9  
    1.10  (* Parsers *)
    1.11  
     2.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Aug 16 13:42:23 2005 +0200
     2.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Aug 16 13:42:26 2005 +0200
     2.3 @@ -954,7 +954,7 @@
     2.4  
     2.5  (* outer syntax *)
     2.6  
     2.7 -local structure P = OuterParse and K = OuterSyntax.Keyword in
     2.8 +local structure P = OuterParse and K = OuterKeyword in
     2.9  
    2.10  val datatype_decl =
    2.11    Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --
     3.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Aug 16 13:42:23 2005 +0200
     3.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Aug 16 13:42:26 2005 +0200
     3.3 @@ -878,7 +878,7 @@
     3.4  
     3.5  (* outer syntax *)
     3.6  
     3.7 -local structure P = OuterParse and K = OuterSyntax.Keyword in
     3.8 +local structure P = OuterParse and K = OuterKeyword in
     3.9  
    3.10  fun mk_ind coind ((sets, intrs), monos) =
    3.11    #1 o add_inductive true coind sets (map P.triple_swap intrs) monos;
     4.1 --- a/src/HOL/Tools/primrec_package.ML	Tue Aug 16 13:42:23 2005 +0200
     4.2 +++ b/src/HOL/Tools/primrec_package.ML	Tue Aug 16 13:42:26 2005 +0200
     4.3 @@ -286,7 +286,7 @@
     4.4  
     4.5  (* outer syntax *)
     4.6  
     4.7 -local structure P = OuterParse and K = OuterSyntax.Keyword in
     4.8 +local structure P = OuterParse and K = OuterKeyword in
     4.9  
    4.10  val primrec_decl =
    4.11    Scan.optional (P.$$$ "(" |-- P.name --| P.$$$ ")") "" --
     5.1 --- a/src/HOL/Tools/recdef_package.ML	Tue Aug 16 13:42:23 2005 +0200
     5.2 +++ b/src/HOL/Tools/recdef_package.ML	Tue Aug 16 13:42:26 2005 +0200
     5.3 @@ -338,7 +338,7 @@
     5.4  
     5.5  (* outer syntax *)
     5.6  
     5.7 -local structure P = OuterParse and K = OuterSyntax.Keyword in
     5.8 +local structure P = OuterParse and K = OuterKeyword in
     5.9  
    5.10  val hints =
    5.11    P.$$$ "(" |-- P.!!! (P.position (P.$$$ "hints" -- P.arguments) --| P.$$$ ")") >> Args.src;
     6.1 --- a/src/HOL/Tools/record_package.ML	Tue Aug 16 13:42:23 2005 +0200
     6.2 +++ b/src/HOL/Tools/record_package.ML	Tue Aug 16 13:42:26 2005 +0200
     6.3 @@ -2131,7 +2131,7 @@
     6.4  
     6.5  (* outer syntax *)
     6.6  
     6.7 -local structure P = OuterParse and K = OuterSyntax.Keyword in
     6.8 +local structure P = OuterParse and K = OuterKeyword in
     6.9  
    6.10  val record_decl =
    6.11    P.type_args -- P.name --
     7.1 --- a/src/HOL/Tools/refute_isar.ML	Tue Aug 16 13:42:23 2005 +0200
     7.2 +++ b/src/HOL/Tools/refute_isar.ML	Tue Aug 16 13:42:26 2005 +0200
     7.3 @@ -54,7 +54,7 @@
     7.4  
     7.5  	fun refute_parser tokens = (refute_scan_args tokens) |>> refute_trans;
     7.6  
     7.7 -	val refute_cmd = OuterSyntax.improper_command "refute" "try to find a model that refutes a given subgoal" OuterSyntax.Keyword.diag refute_parser;
     7.8 +	val refute_cmd = OuterSyntax.improper_command "refute" "try to find a model that refutes a given subgoal" OuterKeyword.diag refute_parser;
     7.9  
    7.10  (* ------------------------------------------------------------------------- *)
    7.11  (* set up the 'refute_params' command                                        *)
    7.12 @@ -90,7 +90,7 @@
    7.13  
    7.14  	fun refute_params_parser tokens = (refute_params_scan_args tokens) |>> refute_params_trans;
    7.15  
    7.16 -	val refute_params_cmd = OuterSyntax.command "refute_params" "show/store default parameters for the 'refute' command" OuterSyntax.Keyword.thy_decl refute_params_parser;
    7.17 +	val refute_params_cmd = OuterSyntax.command "refute_params" "show/store default parameters for the 'refute' command" OuterKeyword.thy_decl refute_params_parser;
    7.18  
    7.19  end;
    7.20  
     8.1 --- a/src/HOL/Tools/specification_package.ML	Tue Aug 16 13:42:23 2005 +0200
     8.2 +++ b/src/HOL/Tools/specification_package.ML	Tue Aug 16 13:42:26 2005 +0200
     8.3 @@ -239,7 +239,7 @@
     8.4  
     8.5  (* outer syntax *)
     8.6  
     8.7 -local structure P = OuterParse and K = OuterSyntax.Keyword in
     8.8 +local structure P = OuterParse and K = OuterKeyword in
     8.9  
    8.10  (* taken from ~~/Pure/Isar/isar_syn.ML *)
    8.11  val opt_overloaded =
     9.1 --- a/src/HOL/Tools/typedef_package.ML	Tue Aug 16 13:42:23 2005 +0200
     9.2 +++ b/src/HOL/Tools/typedef_package.ML	Tue Aug 16 13:42:26 2005 +0200
     9.3 @@ -364,7 +364,7 @@
     9.4  
     9.5  (** outer syntax **)
     9.6  
     9.7 -local structure P = OuterParse and K = OuterSyntax.Keyword in
     9.8 +local structure P = OuterParse and K = OuterKeyword in
     9.9  
    9.10  val typedeclP =
    9.11    OuterSyntax.command "typedecl" "type declaration (HOL)" K.thy_decl
    10.1 --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Tue Aug 16 13:42:23 2005 +0200
    10.2 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Tue Aug 16 13:42:26 2005 +0200
    10.3 @@ -489,7 +489,7 @@
    10.4  
    10.5  (* parsers *)
    10.6  
    10.7 -local structure P = OuterParse and K = OuterSyntax.Keyword in
    10.8 +local structure P = OuterParse and K = OuterKeyword in
    10.9  
   10.10  val actionlist = P.list1 P.term;
   10.11  val inputslist = P.$$$ "inputs" |-- actionlist;
    11.1 --- a/src/HOLCF/cont_consts.ML	Tue Aug 16 13:42:23 2005 +0200
    11.2 +++ b/src/HOLCF/cont_consts.ML	Tue Aug 16 13:42:26 2005 +0200
    11.3 @@ -97,7 +97,7 @@
    11.4  
    11.5  (* outer syntax *)
    11.6  
    11.7 -local structure P = OuterParse and K = OuterSyntax.Keyword in
    11.8 +local structure P = OuterParse and K = OuterKeyword in
    11.9  
   11.10  val constsP =
   11.11    OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl
    12.1 --- a/src/HOLCF/domain/extender.ML	Tue Aug 16 13:42:23 2005 +0200
    12.2 +++ b/src/HOLCF/domain/extender.ML	Tue Aug 16 13:42:26 2005 +0200
    12.3 @@ -140,7 +140,7 @@
    12.4  
    12.5  (** outer syntax **)
    12.6  
    12.7 -local structure P = OuterParse and K = OuterSyntax.Keyword in
    12.8 +local structure P = OuterParse and K = OuterKeyword in
    12.9  
   12.10  val dest_decl =
   12.11    P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
    13.1 --- a/src/HOLCF/fixrec_package.ML	Tue Aug 16 13:42:23 2005 +0200
    13.2 +++ b/src/HOLCF/fixrec_package.ML	Tue Aug 16 13:42:26 2005 +0200
    13.3 @@ -296,7 +296,7 @@
    13.4  (******************************** Parsers ********************************)
    13.5  (*************************************************************************)
    13.6  
    13.7 -local structure P = OuterParse and K = OuterSyntax.Keyword in
    13.8 +local structure P = OuterParse and K = OuterKeyword in
    13.9  
   13.10  val fixrec_eqn = P.opt_thm_name ":" -- P.prop;
   13.11  
    14.1 --- a/src/HOLCF/pcpodef_package.ML	Tue Aug 16 13:42:23 2005 +0200
    14.2 +++ b/src/HOLCF/pcpodef_package.ML	Tue Aug 16 13:42:26 2005 +0200
    14.3 @@ -185,7 +185,7 @@
    14.4  
    14.5  (** outer syntax **)
    14.6  
    14.7 -local structure P = OuterParse and K = OuterSyntax.Keyword in
    14.8 +local structure P = OuterParse and K = OuterKeyword in
    14.9  
   14.10  (* copied from HOL/Tools/typedef_package.ML *)
   14.11  val typedef_proof_decl =
    15.1 --- a/src/Provers/classical.ML	Tue Aug 16 13:42:23 2005 +0200
    15.2 +++ b/src/Provers/classical.ML	Tue Aug 16 13:42:26 2005 +0200
    15.3 @@ -1062,7 +1062,7 @@
    15.4  
    15.5  val print_clasetP =
    15.6    OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner"
    15.7 -    OuterSyntax.Keyword.diag
    15.8 +    OuterKeyword.diag
    15.9      (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep
   15.10        (Toplevel.node_case print_claset (print_local_claset o Proof.context_of)))));
   15.11  
    16.1 --- a/src/Pure/Proof/extraction.ML	Tue Aug 16 13:42:23 2005 +0200
    16.2 +++ b/src/Pure/Proof/extraction.ML	Tue Aug 16 13:42:26 2005 +0200
    16.3 @@ -761,7 +761,7 @@
    16.4  
    16.5  (**** interface ****)
    16.6  
    16.7 -structure P = OuterParse and K = OuterSyntax.Keyword;
    16.8 +structure P = OuterParse and K = OuterKeyword;
    16.9  
   16.10  val parse_vars = Scan.optional (P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") [];
   16.11  
    17.1 --- a/src/Pure/axclass.ML	Tue Aug 16 13:42:23 2005 +0200
    17.2 +++ b/src/Pure/axclass.ML	Tue Aug 16 13:42:26 2005 +0200
    17.3 @@ -362,7 +362,7 @@
    17.4  
    17.5  (** outer syntax **)
    17.6  
    17.7 -local structure P = OuterParse and K = OuterSyntax.Keyword in
    17.8 +local structure P = OuterParse and K = OuterKeyword in
    17.9  
   17.10  val axclassP =
   17.11    OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
    18.1 --- a/src/Pure/codegen.ML	Tue Aug 16 13:42:23 2005 +0200
    18.2 +++ b/src/Pure/codegen.ML	Tue Aug 16 13:42:26 2005 +0200
    18.3 @@ -896,7 +896,7 @@
    18.4         \  in (fn x => !f x) end;\n")]))]];
    18.5  
    18.6  
    18.7 -structure P = OuterParse and K = OuterSyntax.Keyword;
    18.8 +structure P = OuterParse and K = OuterKeyword;
    18.9  
   18.10  fun strip_newlines s = implode (fst (take_suffix (equal "\n")
   18.11    (snd (take_prefix (equal "\n") (explode s))))) ^ "\n";
    19.1 --- a/src/Pure/proof_general.ML	Tue Aug 16 13:42:23 2005 +0200
    19.2 +++ b/src/Pure/proof_general.ML	Tue Aug 16 13:42:26 2005 +0200
    19.3 @@ -1369,7 +1369,7 @@
    19.4  
    19.5  (* additional outer syntax for Isar *)
    19.6  
    19.7 -local structure P = OuterParse and K = OuterSyntax.Keyword in
    19.8 +local structure P = OuterParse and K = OuterKeyword in
    19.9  
   19.10  val undoP = (*undo without output*)
   19.11    OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
   19.12 @@ -1483,7 +1483,7 @@
   19.13    \;;\n" ^
   19.14    defconst "major" (map #1 commands) ^
   19.15    defconst "minor" (List.filter Syntax.is_identifier keywords) ^
   19.16 -  implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^
   19.17 +  implode (map (make_elisp_commands commands) OuterKeyword.kinds) ^
   19.18    "\n(provide 'isar-keywords)\n";
   19.19  
   19.20  in
    20.1 --- a/src/ZF/Tools/datatype_package.ML	Tue Aug 16 13:42:23 2005 +0200
    20.2 +++ b/src/ZF/Tools/datatype_package.ML	Tue Aug 16 13:42:26 2005 +0200
    20.3 @@ -418,7 +418,7 @@
    20.4  
    20.5  (* outer syntax *)
    20.6  
    20.7 -local structure P = OuterParse and K = OuterSyntax.Keyword in
    20.8 +local structure P = OuterParse and K = OuterKeyword in
    20.9  
   20.10  fun mk_datatype ((((dom, dts), monos), type_intrs), type_elims) =
   20.11    #1 o add_datatype (dom, map fst dts) (map snd dts) (monos, type_intrs, type_elims);
    21.1 --- a/src/ZF/Tools/ind_cases.ML	Tue Aug 16 13:42:23 2005 +0200
    21.2 +++ b/src/ZF/Tools/ind_cases.ML	Tue Aug 16 13:42:26 2005 +0200
    21.3 @@ -79,7 +79,7 @@
    21.4  
    21.5  (* outer syntax *)
    21.6  
    21.7 -local structure P = OuterParse and K = OuterSyntax.Keyword in
    21.8 +local structure P = OuterParse and K = OuterKeyword in
    21.9  
   21.10  val ind_cases =
   21.11    P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop)
    22.1 --- a/src/ZF/Tools/induct_tacs.ML	Tue Aug 16 13:42:23 2005 +0200
    22.2 +++ b/src/ZF/Tools/induct_tacs.ML	Tue Aug 16 13:42:26 2005 +0200
    22.3 @@ -200,7 +200,7 @@
    22.4  
    22.5  (* outer syntax *)
    22.6  
    22.7 -local structure P = OuterParse and K = OuterSyntax.Keyword in
    22.8 +local structure P = OuterParse and K = OuterKeyword in
    22.9  
   22.10  val rep_datatype_decl =
   22.11    (P.$$$ "elimination" |-- P.!!! P.xthm) --
    23.1 --- a/src/ZF/Tools/inductive_package.ML	Tue Aug 16 13:42:23 2005 +0200
    23.2 +++ b/src/ZF/Tools/inductive_package.ML	Tue Aug 16 13:42:26 2005 +0200
    23.3 @@ -596,7 +596,7 @@
    23.4  
    23.5  (* outer syntax *)
    23.6  
    23.7 -local structure P = OuterParse and K = OuterSyntax.Keyword in
    23.8 +local structure P = OuterParse and K = OuterKeyword in
    23.9  
   23.10  fun mk_ind (((((doms, intrs), monos), con_defs), type_intrs), type_elims) =
   23.11    #1 o add_inductive doms (map P.triple_swap intrs) (monos, con_defs, type_intrs, type_elims);
    24.1 --- a/src/ZF/Tools/primrec_package.ML	Tue Aug 16 13:42:23 2005 +0200
    24.2 +++ b/src/ZF/Tools/primrec_package.ML	Tue Aug 16 13:42:26 2005 +0200
    24.3 @@ -200,7 +200,7 @@
    24.4  
    24.5  (* outer syntax *)
    24.6  
    24.7 -local structure P = OuterParse and K = OuterSyntax.Keyword in
    24.8 +local structure P = OuterParse and K = OuterKeyword in
    24.9  
   24.10  val primrec_decl = Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
   24.11  
    25.1 --- a/src/ZF/Tools/typechk.ML	Tue Aug 16 13:42:23 2005 +0200
    25.2 +++ b/src/ZF/Tools/typechk.ML	Tue Aug 16 13:42:26 2005 +0200
    25.3 @@ -220,7 +220,7 @@
    25.4  
    25.5  val print_tcsetP =
    25.6    OuterSyntax.improper_command "print_tcset" "print context of ZF type-checker"
    25.7 -    OuterSyntax.Keyword.diag
    25.8 +    OuterKeyword.diag
    25.9      (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep
   25.10        (Toplevel.node_case print_tcset (LocalTypecheckingData.print o Proof.context_of)))));
   25.11