refer directly to structure Keyword and Parse;
authorwenzelm
Sat May 15 23:16:32 2010 +0200 (2010-05-15 ago)
changeset 3695075b8f26f2f07
parent 36949 080e85d46108
child 36951 985c197f2fe9
refer directly to structure Keyword and Parse;
eliminated old-style structure aliases K and P;
src/Pure/Isar/args.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_document.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/method.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/rule_insts.ML
src/Pure/Isar/spec_parse.ML
src/Pure/Isar/toplevel.ML
src/Pure/Isar/value_parse.ML
src/Pure/ML/ml_antiquote.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_thms.ML
src/Pure/Proof/extraction.ML
src/Pure/ProofGeneral/pgip_parser.ML
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/System/isabelle_process.ML
src/Pure/System/isar.ML
src/Pure/System/session.ML
src/Pure/Thy/term_style.ML
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_output.ML
src/Pure/Thy/thy_syntax.ML
src/Pure/Tools/find_consts.ML
src/Pure/Tools/find_theorems.ML
src/Pure/codegen.ML
     1.1 --- a/src/Pure/Isar/args.ML	Sat May 15 22:24:25 2010 +0200
     1.2 +++ b/src/Pure/Isar/args.ML	Sat May 15 23:16:32 2010 +0200
     1.3 @@ -71,7 +71,6 @@
     1.4  struct
     1.5  
     1.6  structure T = OuterLex;
     1.7 -structure P = OuterParse;
     1.8  
     1.9  type token = T.token;
    1.10  
    1.11 @@ -125,17 +124,17 @@
    1.12  
    1.13  (* basic *)
    1.14  
    1.15 -fun token atom = Scan.ahead P.not_eof --| atom;
    1.16 +fun token atom = Scan.ahead Parse.not_eof --| atom;
    1.17  
    1.18  val ident = token
    1.19 -  (P.short_ident || P.long_ident || P.sym_ident || P.term_var ||
    1.20 -    P.type_ident || P.type_var || P.number);
    1.21 +  (Parse.short_ident || Parse.long_ident || Parse.sym_ident || Parse.term_var ||
    1.22 +    Parse.type_ident || Parse.type_var || Parse.number);
    1.23  
    1.24 -val string = token (P.string || P.verbatim);
    1.25 -val alt_string = token P.alt_string;
    1.26 -val symbolic = token P.keyword_ident_or_symbolic;
    1.27 +val string = token (Parse.string || Parse.verbatim);
    1.28 +val alt_string = token Parse.alt_string;
    1.29 +val symbolic = token Parse.keyword_ident_or_symbolic;
    1.30  
    1.31 -fun $$$ x = (ident >> T.content_of || P.keyword)
    1.32 +fun $$$ x = (ident >> T.content_of || Parse.keyword)
    1.33    :|-- (fn y => if x = y then Scan.succeed x else Scan.fail);
    1.34  
    1.35  
    1.36 @@ -158,7 +157,7 @@
    1.37  val name_source_position = named >> T.source_position_of;
    1.38  
    1.39  val name = named >> T.content_of;
    1.40 -val binding = P.position name >> Binding.make;
    1.41 +val binding = Parse.position name >> Binding.make;
    1.42  val alt_name = alt_string >> T.content_of;
    1.43  val symbol = symbolic >> T.content_of;
    1.44  val liberal_name = symbol || name;
    1.45 @@ -216,12 +215,12 @@
    1.46  (* improper method arguments *)
    1.47  
    1.48  val from_to =
    1.49 -  P.nat -- ($$$ "-" |-- P.nat) >> (fn (i, j) => fn tac => Seq.INTERVAL tac i j) ||
    1.50 -  P.nat --| $$$ "-" >> (fn i => fn tac => fn st => Seq.INTERVAL tac i (Thm.nprems_of st) st) ||
    1.51 -  P.nat >> (fn i => fn tac => tac i) ||
    1.52 +  Parse.nat -- ($$$ "-" |-- Parse.nat) >> (fn (i, j) => fn tac => Seq.INTERVAL tac i j) ||
    1.53 +  Parse.nat --| $$$ "-" >> (fn i => fn tac => fn st => Seq.INTERVAL tac i (Thm.nprems_of st) st) ||
    1.54 +  Parse.nat >> (fn i => fn tac => tac i) ||
    1.55    $$$ "!" >> K ALLGOALS;
    1.56  
    1.57 -val goal = $$$ "[" |-- P.!!! (from_to --| $$$ "]");
    1.58 +val goal = $$$ "[" |-- Parse.!!! (from_to --| $$$ "]");
    1.59  fun goal_spec x = Scan.lift (Scan.optional goal (fn tac => tac 1)) x;
    1.60  
    1.61  
    1.62 @@ -229,10 +228,10 @@
    1.63  
    1.64  fun parse_args is_symid =
    1.65    let
    1.66 -    val keyword_symid = token (P.keyword_with is_symid);
    1.67 -    fun atom blk = P.group "argument"
    1.68 +    val keyword_symid = token (Parse.keyword_with is_symid);
    1.69 +    fun atom blk = Parse.group "argument"
    1.70        (ident || keyword_symid || string || alt_string ||
    1.71 -        (if blk then token (P.$$$ ",") else Scan.fail));
    1.72 +        (if blk then token (Parse.$$$ ",") else Scan.fail));
    1.73  
    1.74      fun args blk x = Scan.optional (args1 blk) [] x
    1.75      and args1 blk x =
    1.76 @@ -240,7 +239,8 @@
    1.77          (Scan.repeat1 (atom blk) ||
    1.78            argsp "(" ")" ||
    1.79            argsp "[" "]")) >> flat) x
    1.80 -    and argsp l r x = (token (P.$$$ l) ::: P.!!! (args true @@@ (token (P.$$$ r) >> single))) x;
    1.81 +    and argsp l r x =
    1.82 +      (token (Parse.$$$ l) ::: Parse.!!! (args true @@@ (token (Parse.$$$ r) >> single))) x;
    1.83    in (args, args1) end;
    1.84  
    1.85  val parse = #1 (parse_args T.ident_or_symbolic) false;
    1.86 @@ -253,8 +253,8 @@
    1.87    let
    1.88      val attrib_name = internal_text || (symbolic || named)
    1.89        >> evaluate T.Text (intern o T.content_of);
    1.90 -    val attrib = P.position (attrib_name -- P.!!! parse) >> src;
    1.91 -  in $$$ "[" |-- P.!!! (P.list attrib --| $$$ "]") end;
    1.92 +    val attrib = Parse.position (attrib_name -- Parse.!!! parse) >> src;
    1.93 +  in $$$ "[" |-- Parse.!!! (Parse.list attrib --| $$$ "]") end;
    1.94  
    1.95  fun opt_attribs intern = Scan.optional (attribs intern) [];
    1.96  
     2.1 --- a/src/Pure/Isar/attrib.ML	Sat May 15 22:24:25 2010 +0200
     2.2 +++ b/src/Pure/Isar/attrib.ML	Sat May 15 23:16:32 2010 +0200
     2.3 @@ -48,7 +48,6 @@
     2.4  struct
     2.5  
     2.6  structure T = OuterLex;
     2.7 -structure P = OuterParse;
     2.8  
     2.9  
    2.10  (* source and bindings *)
    2.11 @@ -168,10 +167,10 @@
    2.12  
    2.13  (** parsing attributed theorems **)
    2.14  
    2.15 -val thm_sel = P.$$$ "(" |-- P.list1
    2.16 - (P.nat --| P.minus -- P.nat >> Facts.FromTo ||
    2.17 -  P.nat --| P.minus >> Facts.From ||
    2.18 -  P.nat >> Facts.Single) --| P.$$$ ")";
    2.19 +val thm_sel = Parse.$$$ "(" |-- Parse.list1
    2.20 + (Parse.nat --| Parse.minus -- Parse.nat >> Facts.FromTo ||
    2.21 +  Parse.nat --| Parse.minus >> Facts.From ||
    2.22 +  Parse.nat >> Facts.Single) --| Parse.$$$ ")";
    2.23  
    2.24  local
    2.25  
    2.26 @@ -184,7 +183,7 @@
    2.27      val get_fact = get o Facts.Fact;
    2.28      fun get_named pos name = get (Facts.Named ((name, pos), NONE));
    2.29    in
    2.30 -    P.$$$ "[" |-- Args.attribs (intern thy) --| P.$$$ "]" >> (fn srcs =>
    2.31 +    Parse.$$$ "[" |-- Args.attribs (intern thy) --| Parse.$$$ "]" >> (fn srcs =>
    2.32        let
    2.33          val atts = map (attribute_i thy) srcs;
    2.34          val (context', th') = Library.apply atts (context, Drule.dummy_thm);
    2.35 @@ -192,7 +191,7 @@
    2.36      ||
    2.37      (Scan.ahead Args.alt_name -- Args.named_fact get_fact
    2.38        >> (fn (s, fact) => ("", Facts.Fact s, fact)) ||
    2.39 -     Scan.ahead (P.position fact_name) :|-- (fn (name, pos) =>
    2.40 +     Scan.ahead (Parse.position fact_name) :|-- (fn (name, pos) =>
    2.41        Args.named_fact (get_named pos) -- Scan.option thm_sel
    2.42          >> (fn (fact, sel) => (name, Facts.Named ((name, pos), sel), fact))))
    2.43      -- Args.opt_attribs (intern thy) >> (fn ((name, thmref, fact), srcs) =>
    2.44 @@ -223,11 +222,11 @@
    2.45  (* rule composition *)
    2.46  
    2.47  val COMP_att =
    2.48 -  Scan.lift (Scan.optional (Args.bracks P.nat) 1) -- thm
    2.49 +  Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- thm
    2.50      >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => Drule.compose_single (A, i, B)));
    2.51  
    2.52  val THEN_att =
    2.53 -  Scan.lift (Scan.optional (Args.bracks P.nat) 1) -- thm
    2.54 +  Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- thm
    2.55      >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)));
    2.56  
    2.57  val OF_att =
    2.58 @@ -267,7 +266,7 @@
    2.59  val eta_long =
    2.60    Thm.rule_attribute (K (Conv.fconv_rule Drule.eta_long_conversion));
    2.61  
    2.62 -val rotated = Scan.optional P.int 1 >> (fn n => Thm.rule_attribute (K (rotate_prems n)));
    2.63 +val rotated = Scan.optional Parse.int 1 >> (fn n => Thm.rule_attribute (K (rotate_prems n)));
    2.64  
    2.65  
    2.66  (* theory setup *)
    2.67 @@ -285,9 +284,9 @@
    2.68      "rename bound variables in abstractions" #>
    2.69    setup (Binding.name "unfolded") unfolded "unfolded definitions" #>
    2.70    setup (Binding.name "folded") folded "folded definitions" #>
    2.71 -  setup (Binding.name "consumes") (Scan.lift (Scan.optional P.nat 1) >> Rule_Cases.consumes)
    2.72 +  setup (Binding.name "consumes") (Scan.lift (Scan.optional Parse.nat 1) >> Rule_Cases.consumes)
    2.73      "number of consumed facts" #>
    2.74 -  setup (Binding.name "constraints") (Scan.lift P.nat >> Rule_Cases.constraints)
    2.75 +  setup (Binding.name "constraints") (Scan.lift Parse.nat >> Rule_Cases.constraints)
    2.76      "number of equality constraints" #>
    2.77    setup (Binding.name "case_names") (Scan.lift (Scan.repeat1 Args.name) >> Rule_Cases.case_names)
    2.78      "named rule cases" #>
    2.79 @@ -295,7 +294,7 @@
    2.80      (Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion)
    2.81      "named conclusion of rule cases" #>
    2.82    setup (Binding.name "params")
    2.83 -    (Scan.lift (P.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params)
    2.84 +    (Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params)
    2.85      "named rule parameters" #>
    2.86    setup (Binding.name "standard") (Scan.succeed (Thm.rule_attribute (K Drule.export_without_context)))
    2.87      "result put into standard form (legacy)" #>
    2.88 @@ -345,13 +344,13 @@
    2.89  
    2.90  local
    2.91  
    2.92 -val equals = P.$$$ "=";
    2.93 +val equals = Parse.$$$ "=";
    2.94  
    2.95  fun scan_value (Config.Bool _) =
    2.96        equals -- Args.$$$ "false" >> K (Config.Bool false) ||
    2.97        equals -- Args.$$$ "true" >> K (Config.Bool true) ||
    2.98        Scan.succeed (Config.Bool true)
    2.99 -  | scan_value (Config.Int _) = equals |-- P.int >> Config.Int
   2.100 +  | scan_value (Config.Int _) = equals |-- Parse.int >> Config.Int
   2.101    | scan_value (Config.String _) = equals |-- Args.name >> Config.String;
   2.102  
   2.103  fun scan_config thy config =
     3.1 --- a/src/Pure/Isar/context_rules.ML	Sat May 15 22:24:25 2010 +0200
     3.2 +++ b/src/Pure/Isar/context_rules.ML	Sat May 15 23:16:32 2010 +0200
     3.3 @@ -203,7 +203,7 @@
     3.4  
     3.5  fun add a b c x =
     3.6    (Scan.lift ((Args.bang >> K a || Args.query >> K c || Scan.succeed b) --
     3.7 -    Scan.option OuterParse.nat) >> (fn (f, n) => f n)) x;
     3.8 +    Scan.option Parse.nat) >> (fn (f, n) => f n)) x;
     3.9  
    3.10  val _ = Context.>> (Context.map_theory
    3.11   (Attrib.setup (Binding.name "intro") (add intro_bang intro intro_query)
     4.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat May 15 22:24:25 2010 +0200
     4.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat May 15 23:16:32 2010 +0200
     4.3 @@ -507,7 +507,7 @@
     4.4  
     4.5  fun check_text (txt, pos) state =
     4.6   (Position.report Markup.doc_source pos;
     4.7 -  ignore (ThyOutput.eval_antiquote (#1 (OuterKeyword.get_lexicons ())) state (txt, pos)));
     4.8 +  ignore (ThyOutput.eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));
     4.9  
    4.10  fun header_markup txt = Toplevel.keep (fn state =>
    4.11    if Toplevel.is_toplevel state then check_text txt state
     5.1 --- a/src/Pure/Isar/isar_document.ML	Sat May 15 22:24:25 2010 +0200
     5.2 +++ b/src/Pure/Isar/isar_document.ML	Sat May 15 23:16:32 2010 +0200
     5.3 @@ -275,27 +275,28 @@
     5.4  
     5.5  (** concrete syntax **)
     5.6  
     5.7 -local structure P = OuterParse structure V = ValueParse in
     5.8 +local structure V = ValueParse in
     5.9  
    5.10  val _ =
    5.11    OuterSyntax.internal_command "Isar.define_command"
    5.12 -    (P.string -- P.string >> (fn (id, text) =>
    5.13 +    (Parse.string -- Parse.string >> (fn (id, text) =>
    5.14        Toplevel.position (Position.id_only id) o
    5.15        Toplevel.imperative (fn () =>
    5.16          define_command id (OuterSyntax.prepare_command (Position.id id) text))));
    5.17  
    5.18  val _ =
    5.19    OuterSyntax.internal_command "Isar.begin_document"
    5.20 -    (P.string -- P.string >> (fn (id, path) =>
    5.21 +    (Parse.string -- Parse.string >> (fn (id, path) =>
    5.22        Toplevel.imperative (fn () => begin_document id (Path.explode path))));
    5.23  
    5.24  val _ =
    5.25    OuterSyntax.internal_command "Isar.end_document"
    5.26 -    (P.string >> (fn id => Toplevel.imperative (fn () => end_document id)));
    5.27 +    (Parse.string >> (fn id => Toplevel.imperative (fn () => end_document id)));
    5.28  
    5.29  val _ =
    5.30    OuterSyntax.internal_command "Isar.edit_document"
    5.31 -    (P.string -- P.string -- V.list (P.string -- (P.string >> SOME) || P.string >> rpair NONE)
    5.32 +    (Parse.string -- Parse.string --
    5.33 +        V.list (Parse.string -- (Parse.string >> SOME) || Parse.string >> rpair NONE)
    5.34        >> (fn ((id, new_id), edits) =>
    5.35          Toplevel.position (Position.id_only new_id) o
    5.36          Toplevel.imperative (fn () => edit_document id new_id edits)));
     6.1 --- a/src/Pure/Isar/isar_syn.ML	Sat May 15 22:24:25 2010 +0200
     6.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat May 15 23:16:32 2010 +0200
     6.3 @@ -7,15 +7,12 @@
     6.4  structure IsarSyn: sig end =
     6.5  struct
     6.6  
     6.7 -structure P = OuterParse and K = OuterKeyword;
     6.8 -
     6.9 -
    6.10  (** keywords **)
    6.11  
    6.12  (*keep keywords consistent with the parsers, otherwise be prepared for
    6.13    unexpected errors*)
    6.14  
    6.15 -val _ = List.app OuterKeyword.keyword
    6.16 +val _ = List.app Keyword.keyword
    6.17   ["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
    6.18    "=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>",
    6.19    "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
    6.20 @@ -30,54 +27,54 @@
    6.21  (** init and exit **)
    6.22  
    6.23  val _ =
    6.24 -  OuterSyntax.command "theory" "begin theory" (K.tag_theory K.thy_begin)
    6.25 +  OuterSyntax.command "theory" "begin theory" (Keyword.tag_theory Keyword.thy_begin)
    6.26      (Thy_Header.args >> (Toplevel.print oo IsarCmd.init_theory));
    6.27  
    6.28  val _ =
    6.29 -  OuterSyntax.command "end" "end (local) theory" (K.tag_theory K.thy_end)
    6.30 +  OuterSyntax.command "end" "end (local) theory" (Keyword.tag_theory Keyword.thy_end)
    6.31      (Scan.succeed (Toplevel.exit o Toplevel.end_local_theory));
    6.32  
    6.33  
    6.34  
    6.35  (** markup commands **)
    6.36  
    6.37 -val _ = OuterSyntax.markup_command ThyOutput.Markup "header" "theory header" K.diag
    6.38 -  (P.doc_source >> IsarCmd.header_markup);
    6.39 +val _ = OuterSyntax.markup_command ThyOutput.Markup "header" "theory header" Keyword.diag
    6.40 +  (Parse.doc_source >> IsarCmd.header_markup);
    6.41  
    6.42  val _ = OuterSyntax.markup_command ThyOutput.Markup "chapter" "chapter heading"
    6.43 -  K.thy_heading (P.opt_target -- P.doc_source >> IsarCmd.local_theory_markup);
    6.44 +  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
    6.45  
    6.46  val _ = OuterSyntax.markup_command ThyOutput.Markup "section" "section heading"
    6.47 -  K.thy_heading (P.opt_target -- P.doc_source >> IsarCmd.local_theory_markup);
    6.48 +  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
    6.49  
    6.50  val _ = OuterSyntax.markup_command ThyOutput.Markup "subsection" "subsection heading"
    6.51 -  K.thy_heading (P.opt_target -- P.doc_source >> IsarCmd.local_theory_markup);
    6.52 +  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
    6.53  
    6.54  val _ =
    6.55    OuterSyntax.markup_command ThyOutput.Markup "subsubsection" "subsubsection heading"
    6.56 -  K.thy_heading (P.opt_target -- P.doc_source >> IsarCmd.local_theory_markup);
    6.57 +  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
    6.58  
    6.59  val _ = OuterSyntax.markup_command ThyOutput.MarkupEnv "text" "formal comment (theory)"
    6.60 -  K.thy_decl (P.opt_target -- P.doc_source >> IsarCmd.local_theory_markup);
    6.61 +  Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
    6.62  
    6.63  val _ = OuterSyntax.markup_command ThyOutput.Verbatim "text_raw" "raw document preparation text"
    6.64 -  K.thy_decl (P.opt_target -- P.doc_source >> IsarCmd.local_theory_markup);
    6.65 +  Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
    6.66  
    6.67  val _ = OuterSyntax.markup_command ThyOutput.Markup "sect" "formal comment (proof)"
    6.68 -  (K.tag_proof K.prf_heading) (P.doc_source >> IsarCmd.proof_markup);
    6.69 +  (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> IsarCmd.proof_markup);
    6.70  
    6.71  val _ = OuterSyntax.markup_command ThyOutput.Markup "subsect" "formal comment (proof)"
    6.72 -  (K.tag_proof K.prf_heading) (P.doc_source >> IsarCmd.proof_markup);
    6.73 +  (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> IsarCmd.proof_markup);
    6.74  
    6.75  val _ = OuterSyntax.markup_command ThyOutput.Markup "subsubsect" "formal comment (proof)"
    6.76 -  (K.tag_proof K.prf_heading) (P.doc_source >> IsarCmd.proof_markup);
    6.77 +  (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> IsarCmd.proof_markup);
    6.78  
    6.79  val _ = OuterSyntax.markup_command ThyOutput.MarkupEnv "txt" "formal comment (proof)"
    6.80 -  (K.tag_proof K.prf_decl) (P.doc_source >> IsarCmd.proof_markup);
    6.81 +  (Keyword.tag_proof Keyword.prf_decl) (Parse.doc_source >> IsarCmd.proof_markup);
    6.82  
    6.83  val _ = OuterSyntax.markup_command ThyOutput.Verbatim "txt_raw"
    6.84 -  "raw document preparation text (proof)" (K.tag_proof K.prf_decl)
    6.85 -  (P.doc_source >> IsarCmd.proof_markup);
    6.86 +  "raw document preparation text (proof)" (Keyword.tag_proof Keyword.prf_decl)
    6.87 +  (Parse.doc_source >> IsarCmd.proof_markup);
    6.88  
    6.89  
    6.90  
    6.91 @@ -86,175 +83,185 @@
    6.92  (* classes and sorts *)
    6.93  
    6.94  val _ =
    6.95 -  OuterSyntax.command "classes" "declare type classes" K.thy_decl
    6.96 -    (Scan.repeat1 (P.binding -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
    6.97 -        P.!!! (P.list1 P.xname)) []) >> (Toplevel.theory o fold AxClass.axiomatize_class_cmd));
    6.98 +  OuterSyntax.command "classes" "declare type classes" Keyword.thy_decl
    6.99 +    (Scan.repeat1 (Parse.binding -- Scan.optional ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |--
   6.100 +        Parse.!!! (Parse.list1 Parse.xname)) [])
   6.101 +      >> (Toplevel.theory o fold AxClass.axiomatize_class_cmd));
   6.102  
   6.103  val _ =
   6.104 -  OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl
   6.105 -    (P.and_list1 (P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname))
   6.106 +  OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" Keyword.thy_decl
   6.107 +    (Parse.and_list1 (Parse.xname -- ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<")
   6.108 +        |-- Parse.!!! Parse.xname))
   6.109      >> (Toplevel.theory o AxClass.axiomatize_classrel_cmd));
   6.110  
   6.111  val _ =
   6.112    OuterSyntax.local_theory "default_sort" "declare default sort for explicit type variables"
   6.113 -    K.thy_decl
   6.114 -    (P.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy));
   6.115 +    Keyword.thy_decl
   6.116 +    (Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy));
   6.117  
   6.118  
   6.119  (* types *)
   6.120  
   6.121  val _ =
   6.122 -  OuterSyntax.local_theory "typedecl" "type declaration" K.thy_decl
   6.123 -    (P.type_args -- P.binding -- P.opt_mixfix
   6.124 +  OuterSyntax.local_theory "typedecl" "type declaration" Keyword.thy_decl
   6.125 +    (Parse.type_args -- Parse.binding -- Parse.opt_mixfix
   6.126        >> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd));
   6.127  
   6.128  val _ =
   6.129 -  OuterSyntax.local_theory "types" "declare type abbreviations" K.thy_decl
   6.130 +  OuterSyntax.local_theory "types" "declare type abbreviations" Keyword.thy_decl
   6.131      (Scan.repeat1
   6.132 -      (P.type_args -- P.binding -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_mixfix')))
   6.133 +      (Parse.type_args -- Parse.binding --
   6.134 +        (Parse.$$$ "=" |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix')))
   6.135        >> (fold (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs)));
   6.136  
   6.137  val _ =
   6.138    OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
   6.139 -    K.thy_decl (Scan.repeat1 P.binding >> (Toplevel.theory o Sign.add_nonterminals));
   6.140 +    Keyword.thy_decl (Scan.repeat1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals));
   6.141  
   6.142  val _ =
   6.143 -  OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl
   6.144 -    (Scan.repeat1 P.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity_cmd));
   6.145 +  OuterSyntax.command "arities" "state type arities (axiomatic!)" Keyword.thy_decl
   6.146 +    (Scan.repeat1 Parse.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity_cmd));
   6.147  
   6.148  
   6.149  (* consts and syntax *)
   6.150  
   6.151  val _ =
   6.152 -  OuterSyntax.command "judgment" "declare object-logic judgment" K.thy_decl
   6.153 -    (P.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
   6.154 +  OuterSyntax.command "judgment" "declare object-logic judgment" Keyword.thy_decl
   6.155 +    (Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
   6.156  
   6.157  val _ =
   6.158 -  OuterSyntax.command "consts" "declare constants" K.thy_decl
   6.159 -    (Scan.repeat1 P.const_binding >> (Toplevel.theory o Sign.add_consts));
   6.160 +  OuterSyntax.command "consts" "declare constants" Keyword.thy_decl
   6.161 +    (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts));
   6.162  
   6.163 -val opt_overloaded = P.opt_keyword "overloaded";
   6.164 +val opt_overloaded = Parse.opt_keyword "overloaded";
   6.165  
   6.166  val _ =
   6.167 -  OuterSyntax.command "finalconsts" "declare constants as final" K.thy_decl
   6.168 -    (opt_overloaded -- Scan.repeat1 P.term >> (uncurry (Toplevel.theory oo Theory.add_finals)));
   6.169 +  OuterSyntax.command "finalconsts" "declare constants as final" Keyword.thy_decl
   6.170 +    (opt_overloaded -- Scan.repeat1 Parse.term >> (uncurry (Toplevel.theory oo Theory.add_finals)));
   6.171  
   6.172  val mode_spec =
   6.173 -  (P.$$$ "output" >> K ("", false)) || P.name -- Scan.optional (P.$$$ "output" >> K false) true;
   6.174 +  (Parse.$$$ "output" >> K ("", false)) ||
   6.175 +    Parse.name -- Scan.optional (Parse.$$$ "output" >> K false) true;
   6.176  
   6.177  val opt_mode =
   6.178 -  Scan.optional (P.$$$ "(" |-- P.!!! (mode_spec --| P.$$$ ")")) Syntax.mode_default;
   6.179 +  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (mode_spec --| Parse.$$$ ")")) Syntax.mode_default;
   6.180  
   6.181  val _ =
   6.182 -  OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl
   6.183 -    (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Sign.add_modesyntax));
   6.184 +  OuterSyntax.command "syntax" "declare syntactic constants" Keyword.thy_decl
   6.185 +    (opt_mode -- Scan.repeat1 Parse.const >> (Toplevel.theory o uncurry Sign.add_modesyntax));
   6.186  
   6.187  val _ =
   6.188 -  OuterSyntax.command "no_syntax" "delete syntax declarations" K.thy_decl
   6.189 -    (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Sign.del_modesyntax));
   6.190 +  OuterSyntax.command "no_syntax" "delete syntax declarations" Keyword.thy_decl
   6.191 +    (opt_mode -- Scan.repeat1 Parse.const >> (Toplevel.theory o uncurry Sign.del_modesyntax));
   6.192  
   6.193  
   6.194  (* translations *)
   6.195  
   6.196  val trans_pat =
   6.197 -  Scan.optional (P.$$$ "(" |-- P.!!! (P.xname --| P.$$$ ")")) "logic" -- P.string;
   6.198 +  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.xname --| Parse.$$$ ")")) "logic"
   6.199 +    -- Parse.string;
   6.200  
   6.201  fun trans_arrow toks =
   6.202 -  ((P.$$$ "\\<rightharpoonup>" || P.$$$ "=>") >> K Syntax.ParseRule ||
   6.203 -    (P.$$$ "\\<leftharpoondown>" || P.$$$ "<=") >> K Syntax.PrintRule ||
   6.204 -    (P.$$$ "\\<rightleftharpoons>" || P.$$$ "==") >> K Syntax.ParsePrintRule) toks;
   6.205 +  ((Parse.$$$ "\\<rightharpoonup>" || Parse.$$$ "=>") >> K Syntax.ParseRule ||
   6.206 +    (Parse.$$$ "\\<leftharpoondown>" || Parse.$$$ "<=") >> K Syntax.PrintRule ||
   6.207 +    (Parse.$$$ "\\<rightleftharpoons>" || Parse.$$$ "==") >> K Syntax.ParsePrintRule) toks;
   6.208  
   6.209  val trans_line =
   6.210 -  trans_pat -- P.!!! (trans_arrow -- trans_pat)
   6.211 +  trans_pat -- Parse.!!! (trans_arrow -- trans_pat)
   6.212      >> (fn (left, (arr, right)) => arr (left, right));
   6.213  
   6.214  val _ =
   6.215 -  OuterSyntax.command "translations" "declare syntax translation rules" K.thy_decl
   6.216 +  OuterSyntax.command "translations" "declare syntax translation rules" Keyword.thy_decl
   6.217      (Scan.repeat1 trans_line >> (Toplevel.theory o Sign.add_trrules));
   6.218  
   6.219  val _ =
   6.220 -  OuterSyntax.command "no_translations" "remove syntax translation rules" K.thy_decl
   6.221 +  OuterSyntax.command "no_translations" "remove syntax translation rules" Keyword.thy_decl
   6.222      (Scan.repeat1 trans_line >> (Toplevel.theory o Sign.del_trrules));
   6.223  
   6.224  
   6.225  (* axioms and definitions *)
   6.226  
   6.227  val _ =
   6.228 -  OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
   6.229 +  OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" Keyword.thy_decl
   6.230      (Scan.repeat1 SpecParse.spec >>
   6.231        (Toplevel.theory o
   6.232          (IsarCmd.add_axioms o
   6.233            tap (fn _ => legacy_feature "Old 'axioms' command -- use 'axiomatization' instead"))));
   6.234  
   6.235  val opt_unchecked_overloaded =
   6.236 -  Scan.optional (P.$$$ "(" |-- P.!!!
   6.237 -    (((P.$$$ "unchecked" >> K true) -- Scan.optional (P.$$$ "overloaded" >> K true) false ||
   6.238 -      P.$$$ "overloaded" >> K (false, true)) --| P.$$$ ")")) (false, false);
   6.239 +  Scan.optional (Parse.$$$ "(" |-- Parse.!!!
   6.240 +    (((Parse.$$$ "unchecked" >> K true) -- Scan.optional (Parse.$$$ "overloaded" >> K true) false ||
   6.241 +      Parse.$$$ "overloaded" >> K (false, true)) --| Parse.$$$ ")")) (false, false);
   6.242  
   6.243  val _ =
   6.244 -  OuterSyntax.command "defs" "define constants" K.thy_decl
   6.245 +  OuterSyntax.command "defs" "define constants" Keyword.thy_decl
   6.246      (opt_unchecked_overloaded --
   6.247 -      Scan.repeat1 (SpecParse.thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y)))
   6.248 +      Scan.repeat1 (SpecParse.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y)))
   6.249        >> (Toplevel.theory o IsarCmd.add_defs));
   6.250  
   6.251  
   6.252  (* old constdefs *)
   6.253  
   6.254  val old_constdecl =
   6.255 -  P.binding --| P.where_ >> (fn x => (x, NONE, NoSyn)) ||
   6.256 -  P.binding -- (P.$$$ "::" |-- P.!!! P.typ >> SOME) -- P.opt_mixfix'
   6.257 -    --| Scan.option P.where_ >> P.triple1 ||
   6.258 -  P.binding -- (P.mixfix >> pair NONE) --| Scan.option P.where_ >> P.triple2;
   6.259 +  Parse.binding --| Parse.where_ >> (fn x => (x, NONE, NoSyn)) ||
   6.260 +  Parse.binding -- (Parse.$$$ "::" |-- Parse.!!! Parse.typ >> SOME) -- Parse.opt_mixfix'
   6.261 +    --| Scan.option Parse.where_ >> Parse.triple1 ||
   6.262 +  Parse.binding -- (Parse.mixfix >> pair NONE) --| Scan.option Parse.where_ >> Parse.triple2;
   6.263  
   6.264 -val old_constdef = Scan.option old_constdecl -- (SpecParse.opt_thm_name ":" -- P.prop);
   6.265 +val old_constdef = Scan.option old_constdecl -- (SpecParse.opt_thm_name ":" -- Parse.prop);
   6.266  
   6.267  val structs =
   6.268 -  Scan.optional ((P.$$$ "(" -- P.$$$ "structure") |-- P.!!! (P.simple_fixes --| P.$$$ ")")) [];
   6.269 +  Scan.optional ((Parse.$$$ "(" -- Parse.$$$ "structure")
   6.270 +    |-- Parse.!!! (Parse.simple_fixes --| Parse.$$$ ")")) [];
   6.271  
   6.272  val _ =
   6.273 -  OuterSyntax.command "constdefs" "old-style constant definition" K.thy_decl
   6.274 +  OuterSyntax.command "constdefs" "old-style constant definition" Keyword.thy_decl
   6.275      (structs -- Scan.repeat1 old_constdef >> (Toplevel.theory o Constdefs.add_constdefs));
   6.276  
   6.277  
   6.278  (* constant definitions and abbreviations *)
   6.279  
   6.280  val _ =
   6.281 -  OuterSyntax.local_theory "definition" "constant definition" K.thy_decl
   6.282 +  OuterSyntax.local_theory "definition" "constant definition" Keyword.thy_decl
   6.283      (SpecParse.constdef >> (fn args => #2 o Specification.definition_cmd args));
   6.284  
   6.285  val _ =
   6.286 -  OuterSyntax.local_theory "abbreviation" "constant abbreviation" K.thy_decl
   6.287 -    (opt_mode -- (Scan.option SpecParse.constdecl -- P.prop)
   6.288 -    >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
   6.289 +  OuterSyntax.local_theory "abbreviation" "constant abbreviation" Keyword.thy_decl
   6.290 +    (opt_mode -- (Scan.option SpecParse.constdecl -- Parse.prop)
   6.291 +      >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
   6.292  
   6.293  val _ =
   6.294 -  OuterSyntax.local_theory "type_notation" "add concrete syntax for type constructors" K.thy_decl
   6.295 -    (opt_mode -- P.and_list1 (P.xname -- P.mixfix)
   6.296 -    >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
   6.297 +  OuterSyntax.local_theory "type_notation" "add concrete syntax for type constructors"
   6.298 +    Keyword.thy_decl
   6.299 +    (opt_mode -- Parse.and_list1 (Parse.xname -- Parse.mixfix)
   6.300 +      >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
   6.301  
   6.302  val _ =
   6.303 -  OuterSyntax.local_theory "no_type_notation" "delete concrete syntax for type constructors" K.thy_decl
   6.304 -    (opt_mode -- P.and_list1 (P.xname -- P.mixfix)
   6.305 -    >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
   6.306 +  OuterSyntax.local_theory "no_type_notation" "delete concrete syntax for type constructors"
   6.307 +    Keyword.thy_decl
   6.308 +    (opt_mode -- Parse.and_list1 (Parse.xname -- Parse.mixfix)
   6.309 +      >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
   6.310  
   6.311  val _ =
   6.312 -  OuterSyntax.local_theory "notation" "add concrete syntax for constants / fixed variables" K.thy_decl
   6.313 -    (opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
   6.314 -    >> (fn (mode, args) => Specification.notation_cmd true mode args));
   6.315 +  OuterSyntax.local_theory "notation" "add concrete syntax for constants / fixed variables"
   6.316 +    Keyword.thy_decl
   6.317 +    (opt_mode -- Parse.and_list1 (Parse.xname -- SpecParse.locale_mixfix)
   6.318 +      >> (fn (mode, args) => Specification.notation_cmd true mode args));
   6.319  
   6.320  val _ =
   6.321 -  OuterSyntax.local_theory "no_notation" "delete concrete syntax for constants / fixed variables" K.thy_decl
   6.322 -    (opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
   6.323 -    >> (fn (mode, args) => Specification.notation_cmd false mode args));
   6.324 +  OuterSyntax.local_theory "no_notation" "delete concrete syntax for constants / fixed variables"
   6.325 +    Keyword.thy_decl
   6.326 +    (opt_mode -- Parse.and_list1 (Parse.xname -- SpecParse.locale_mixfix)
   6.327 +      >> (fn (mode, args) => Specification.notation_cmd false mode args));
   6.328  
   6.329  
   6.330  (* constant specifications *)
   6.331  
   6.332  val _ =
   6.333 -  OuterSyntax.command "axiomatization" "axiomatic constant specification" K.thy_decl
   6.334 -    (Scan.optional P.fixes [] --
   6.335 -      Scan.optional (P.where_ |-- P.!!! (P.and_list1 SpecParse.specs)) []
   6.336 -    >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));
   6.337 +  OuterSyntax.command "axiomatization" "axiomatic constant specification" Keyword.thy_decl
   6.338 +    (Scan.optional Parse.fixes [] --
   6.339 +      Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 SpecParse.specs)) []
   6.340 +      >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));
   6.341  
   6.342  
   6.343  (* theorems *)
   6.344 @@ -263,30 +270,30 @@
   6.345    SpecParse.name_facts >> (fn args => #2 o Specification.theorems_cmd kind args);
   6.346  
   6.347  val _ =
   6.348 -  OuterSyntax.local_theory "theorems" "define theorems" K.thy_decl (theorems Thm.theoremK);
   6.349 +  OuterSyntax.local_theory "theorems" "define theorems" Keyword.thy_decl (theorems Thm.theoremK);
   6.350  
   6.351  val _ =
   6.352 -  OuterSyntax.local_theory "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK);
   6.353 +  OuterSyntax.local_theory "lemmas" "define lemmas" Keyword.thy_decl (theorems Thm.lemmaK);
   6.354  
   6.355  val _ =
   6.356 -  OuterSyntax.local_theory "declare" "declare theorems" K.thy_decl
   6.357 -    (P.and_list1 SpecParse.xthms1
   6.358 +  OuterSyntax.local_theory "declare" "declare theorems" Keyword.thy_decl
   6.359 +    (Parse.and_list1 SpecParse.xthms1
   6.360        >> (fn args => #2 o Specification.theorems_cmd "" [(Attrib.empty_binding, flat args)]));
   6.361  
   6.362  
   6.363  (* name space entry path *)
   6.364  
   6.365  val _ =
   6.366 -  OuterSyntax.command "global" "disable prefixing of theory name" K.thy_decl
   6.367 +  OuterSyntax.command "global" "disable prefixing of theory name" Keyword.thy_decl
   6.368      (Scan.succeed (Toplevel.theory Sign.root_path));
   6.369  
   6.370  val _ =
   6.371 -  OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl
   6.372 +  OuterSyntax.command "local" "enable prefixing of theory name" Keyword.thy_decl
   6.373      (Scan.succeed (Toplevel.theory Sign.local_path));
   6.374  
   6.375  fun hide_names name hide what =
   6.376 -  OuterSyntax.command name ("hide " ^ what ^ " from name space") K.thy_decl
   6.377 -    ((P.opt_keyword "open" >> not) -- Scan.repeat1 P.xname >>
   6.378 +  OuterSyntax.command name ("hide " ^ what ^ " from name space") Keyword.thy_decl
   6.379 +    ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 Parse.xname >>
   6.380        (Toplevel.theory o uncurry hide));
   6.381  
   6.382  val _ = hide_names "hide_class" IsarCmd.hide_class "classes";
   6.383 @@ -305,101 +312,104 @@
   6.384    (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf;
   6.385  
   6.386  val _ =
   6.387 -  OuterSyntax.command "use" "ML text from file" (K.tag_ml K.thy_decl)
   6.388 -    (P.path >> (fn path => Toplevel.generic_theory (ThyInfo.exec_file false path #> propagate_env)));
   6.389 +  OuterSyntax.command "use" "ML text from file" (Keyword.tag_ml Keyword.thy_decl)
   6.390 +    (Parse.path >>
   6.391 +      (fn path => Toplevel.generic_theory (ThyInfo.exec_file false path #> propagate_env)));
   6.392  
   6.393  val _ =
   6.394 -  OuterSyntax.command "ML" "ML text within theory or local theory" (K.tag_ml K.thy_decl)
   6.395 -    (P.ML_source >> (fn (txt, pos) =>
   6.396 +  OuterSyntax.command "ML" "ML text within theory or local theory"
   6.397 +    (Keyword.tag_ml Keyword.thy_decl)
   6.398 +    (Parse.ML_source >> (fn (txt, pos) =>
   6.399        Toplevel.generic_theory
   6.400          (ML_Context.exec (fn () => ML_Context.eval true pos txt) #> propagate_env)));
   6.401  
   6.402  val _ =
   6.403 -  OuterSyntax.command "ML_prf" "ML text within proof" (K.tag_proof K.prf_decl)
   6.404 -    (P.ML_source >> (fn (txt, pos) =>
   6.405 +  OuterSyntax.command "ML_prf" "ML text within proof" (Keyword.tag_proof Keyword.prf_decl)
   6.406 +    (Parse.ML_source >> (fn (txt, pos) =>
   6.407        Toplevel.proof (Proof.map_context (Context.proof_map
   6.408          (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf)));
   6.409  
   6.410  val _ =
   6.411 -  OuterSyntax.command "ML_val" "diagnostic ML text" (K.tag_ml K.diag)
   6.412 -    (P.ML_source >> IsarCmd.ml_diag true);
   6.413 +  OuterSyntax.command "ML_val" "diagnostic ML text" (Keyword.tag_ml Keyword.diag)
   6.414 +    (Parse.ML_source >> IsarCmd.ml_diag true);
   6.415  
   6.416  val _ =
   6.417 -  OuterSyntax.command "ML_command" "diagnostic ML text (silent)" (K.tag_ml K.diag)
   6.418 -    (P.ML_source >> (Toplevel.no_timing oo IsarCmd.ml_diag false));
   6.419 +  OuterSyntax.command "ML_command" "diagnostic ML text (silent)" (Keyword.tag_ml Keyword.diag)
   6.420 +    (Parse.ML_source >> (Toplevel.no_timing oo IsarCmd.ml_diag false));
   6.421  
   6.422  val _ =
   6.423 -  OuterSyntax.command "setup" "ML theory setup" (K.tag_ml K.thy_decl)
   6.424 -    (P.ML_source >> (Toplevel.theory o IsarCmd.global_setup));
   6.425 +  OuterSyntax.command "setup" "ML theory setup" (Keyword.tag_ml Keyword.thy_decl)
   6.426 +    (Parse.ML_source >> (Toplevel.theory o IsarCmd.global_setup));
   6.427  
   6.428  val _ =
   6.429 -  OuterSyntax.local_theory "local_setup" "ML local theory setup" (K.tag_ml K.thy_decl)
   6.430 -    (P.ML_source >> IsarCmd.local_setup);
   6.431 +  OuterSyntax.local_theory "local_setup" "ML local theory setup" (Keyword.tag_ml Keyword.thy_decl)
   6.432 +    (Parse.ML_source >> IsarCmd.local_setup);
   6.433  
   6.434  val _ =
   6.435 -  OuterSyntax.command "attribute_setup" "define attribute in ML" (K.tag_ml K.thy_decl)
   6.436 -    (P.position P.name -- P.!!! (P.$$$ "=" |-- P.ML_source -- P.text)
   6.437 -    >> (fn (name, (txt, cmt)) => Toplevel.theory (Attrib.attribute_setup name txt cmt)));
   6.438 +  OuterSyntax.command "attribute_setup" "define attribute in ML" (Keyword.tag_ml Keyword.thy_decl)
   6.439 +    (Parse.position Parse.name -- Parse.!!! (Parse.$$$ "=" |-- Parse.ML_source -- Parse.text)
   6.440 +      >> (fn (name, (txt, cmt)) => Toplevel.theory (Attrib.attribute_setup name txt cmt)));
   6.441  
   6.442  val _ =
   6.443 -  OuterSyntax.command "method_setup" "define proof method in ML" (K.tag_ml K.thy_decl)
   6.444 -    (P.position P.name -- P.!!! (P.$$$ "=" |-- P.ML_source -- P.text)
   6.445 -    >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
   6.446 +  OuterSyntax.command "method_setup" "define proof method in ML" (Keyword.tag_ml Keyword.thy_decl)
   6.447 +    (Parse.position Parse.name -- Parse.!!! (Parse.$$$ "=" |-- Parse.ML_source -- Parse.text)
   6.448 +      >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
   6.449  
   6.450  val _ =
   6.451 -  OuterSyntax.local_theory "declaration" "generic ML declaration" (K.tag_ml K.thy_decl)
   6.452 -    (P.opt_keyword "pervasive" -- P.ML_source >> uncurry IsarCmd.declaration);
   6.453 +  OuterSyntax.local_theory "declaration" "generic ML declaration" (Keyword.tag_ml Keyword.thy_decl)
   6.454 +    (Parse.opt_keyword "pervasive" -- Parse.ML_source >> uncurry IsarCmd.declaration);
   6.455  
   6.456  val _ =
   6.457 -  OuterSyntax.local_theory "simproc_setup" "define simproc in ML" (K.tag_ml K.thy_decl)
   6.458 -    (P.name -- (P.$$$ "(" |-- P.enum1 "|" P.term --| P.$$$ ")" --| P.$$$ "=") --
   6.459 -      P.ML_source -- Scan.optional (P.$$$ "identifier" |-- Scan.repeat1 P.xname) []
   6.460 +  OuterSyntax.local_theory "simproc_setup" "define simproc in ML" (Keyword.tag_ml Keyword.thy_decl)
   6.461 +    (Parse.name --
   6.462 +      (Parse.$$$ "(" |-- Parse.enum1 "|" Parse.term --| Parse.$$$ ")" --| Parse.$$$ "=") --
   6.463 +      Parse.ML_source -- Scan.optional (Parse.$$$ "identifier" |-- Scan.repeat1 Parse.xname) []
   6.464      >> (fn (((a, b), c), d) => IsarCmd.simproc_setup a b c d));
   6.465  
   6.466  
   6.467  (* translation functions *)
   6.468  
   6.469 -val trfun = P.opt_keyword "advanced" -- P.ML_source;
   6.470 +val trfun = Parse.opt_keyword "advanced" -- Parse.ML_source;
   6.471  
   6.472  val _ =
   6.473    OuterSyntax.command "parse_ast_translation" "install parse ast translation functions"
   6.474 -    (K.tag_ml K.thy_decl)
   6.475 +    (Keyword.tag_ml Keyword.thy_decl)
   6.476      (trfun >> (Toplevel.theory o IsarCmd.parse_ast_translation));
   6.477  
   6.478  val _ =
   6.479    OuterSyntax.command "parse_translation" "install parse translation functions"
   6.480 -    (K.tag_ml K.thy_decl)
   6.481 +    (Keyword.tag_ml Keyword.thy_decl)
   6.482      (trfun >> (Toplevel.theory o IsarCmd.parse_translation));
   6.483  
   6.484  val _ =
   6.485    OuterSyntax.command "print_translation" "install print translation functions"
   6.486 -    (K.tag_ml K.thy_decl)
   6.487 +    (Keyword.tag_ml Keyword.thy_decl)
   6.488      (trfun >> (Toplevel.theory o IsarCmd.print_translation));
   6.489  
   6.490  val _ =
   6.491    OuterSyntax.command "typed_print_translation" "install typed print translation functions"
   6.492 -    (K.tag_ml K.thy_decl)
   6.493 +    (Keyword.tag_ml Keyword.thy_decl)
   6.494      (trfun >> (Toplevel.theory o IsarCmd.typed_print_translation));
   6.495  
   6.496  val _ =
   6.497    OuterSyntax.command "print_ast_translation" "install print ast translation functions"
   6.498 -    (K.tag_ml K.thy_decl)
   6.499 +    (Keyword.tag_ml Keyword.thy_decl)
   6.500      (trfun >> (Toplevel.theory o IsarCmd.print_ast_translation));
   6.501  
   6.502  
   6.503  (* oracles *)
   6.504  
   6.505  val _ =
   6.506 -  OuterSyntax.command "oracle" "declare oracle" (K.tag_ml K.thy_decl)
   6.507 -    (P.position P.name -- (P.$$$ "=" |-- P.ML_source) >>
   6.508 +  OuterSyntax.command "oracle" "declare oracle" (Keyword.tag_ml Keyword.thy_decl)
   6.509 +    (Parse.position Parse.name -- (Parse.$$$ "=" |-- Parse.ML_source) >>
   6.510        (fn (x, y) => Toplevel.theory (IsarCmd.oracle x y)));
   6.511  
   6.512  
   6.513  (* local theories *)
   6.514  
   6.515  val _ =
   6.516 -  OuterSyntax.command "context" "enter local theory context" K.thy_decl
   6.517 -    (P.name --| P.begin >> (fn name =>
   6.518 +  OuterSyntax.command "context" "enter local theory context" Keyword.thy_decl
   6.519 +    (Parse.name --| Parse.begin >> (fn name =>
   6.520        Toplevel.print o Toplevel.begin_local_theory true (Theory_Target.context_cmd name)));
   6.521  
   6.522  
   6.523 @@ -407,36 +417,38 @@
   6.524  
   6.525  val locale_val =
   6.526    SpecParse.locale_expression false --
   6.527 -    Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
   6.528 +    Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
   6.529    Scan.repeat1 SpecParse.context_element >> pair ([], []);
   6.530  
   6.531  val _ =
   6.532 -  OuterSyntax.command "locale" "define named proof context" K.thy_decl
   6.533 -    (P.binding -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (([], []), []) -- P.opt_begin
   6.534 +  OuterSyntax.command "locale" "define named proof context" Keyword.thy_decl
   6.535 +    (Parse.binding --
   6.536 +      Scan.optional (Parse.$$$ "=" |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
   6.537        >> (fn ((name, (expr, elems)), begin) =>
   6.538            (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
   6.539              (Expression.add_locale_cmd name Binding.empty expr elems #> snd)));
   6.540  
   6.541  val _ =
   6.542    OuterSyntax.command "sublocale"
   6.543 -    "prove sublocale relation between a locale and a locale expression" K.thy_goal
   6.544 -    (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! (SpecParse.locale_expression false)
   6.545 +    "prove sublocale relation between a locale and a locale expression" Keyword.thy_goal
   6.546 +    (Parse.xname --| (Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") --
   6.547 +      Parse.!!! (SpecParse.locale_expression false)
   6.548        >> (fn (loc, expr) =>
   6.549            Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr)));
   6.550  
   6.551  val _ =
   6.552    OuterSyntax.command "interpretation"
   6.553 -    "prove interpretation of locale expression in theory" K.thy_goal
   6.554 -    (P.!!! (SpecParse.locale_expression true) --
   6.555 -      Scan.optional (P.where_ |-- P.and_list1 (SpecParse.opt_thm_name ":" -- P.prop)) []
   6.556 +    "prove interpretation of locale expression in theory" Keyword.thy_goal
   6.557 +    (Parse.!!! (SpecParse.locale_expression true) --
   6.558 +      Scan.optional (Parse.where_ |-- Parse.and_list1 (SpecParse.opt_thm_name ":" -- Parse.prop)) []
   6.559        >> (fn (expr, equations) => Toplevel.print o
   6.560            Toplevel.theory_to_proof (Expression.interpretation_cmd expr equations)));
   6.561  
   6.562  val _ =
   6.563    OuterSyntax.command "interpret"
   6.564      "prove interpretation of locale expression in proof context"
   6.565 -    (K.tag_proof K.prf_goal)
   6.566 -    (P.!!! (SpecParse.locale_expression true)
   6.567 +    (Keyword.tag_proof Keyword.prf_goal)
   6.568 +    (Parse.!!! (SpecParse.locale_expression true)
   6.569        >> (fn expr => Toplevel.print o Toplevel.proof' (Expression.interpret_cmd expr)));
   6.570  
   6.571  
   6.572 @@ -444,41 +456,43 @@
   6.573  
   6.574  val class_val =
   6.575    SpecParse.class_expr --
   6.576 -    Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
   6.577 +    Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
   6.578    Scan.repeat1 SpecParse.context_element >> pair [];
   6.579  
   6.580  val _ =
   6.581 -  OuterSyntax.command "class" "define type class" K.thy_decl
   6.582 -   (P.binding -- Scan.optional (P.$$$ "=" |-- class_val) ([], []) -- P.opt_begin
   6.583 +  OuterSyntax.command "class" "define type class" Keyword.thy_decl
   6.584 +   (Parse.binding -- Scan.optional (Parse.$$$ "=" |-- class_val) ([], []) -- Parse.opt_begin
   6.585      >> (fn ((name, (supclasses, elems)), begin) =>
   6.586          (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
   6.587            (Class.class_cmd name supclasses elems #> snd)));
   6.588  
   6.589  val _ =
   6.590 -  OuterSyntax.local_theory_to_proof "subclass" "prove a subclass relation" K.thy_goal
   6.591 -    (P.xname >> Class.subclass_cmd);
   6.592 +  OuterSyntax.local_theory_to_proof "subclass" "prove a subclass relation" Keyword.thy_goal
   6.593 +    (Parse.xname >> Class.subclass_cmd);
   6.594  
   6.595  val _ =
   6.596 -  OuterSyntax.command "instantiation" "instantiate and prove type arity" K.thy_decl
   6.597 -   (P.multi_arity --| P.begin
   6.598 +  OuterSyntax.command "instantiation" "instantiate and prove type arity" Keyword.thy_decl
   6.599 +   (Parse.multi_arity --| Parse.begin
   6.600       >> (fn arities => Toplevel.print o
   6.601           Toplevel.begin_local_theory true (Theory_Target.instantiation_cmd arities)));
   6.602  
   6.603  val _ =
   6.604 -  OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
   6.605 -  ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> Class.classrel_cmd ||
   6.606 -    P.multi_arity >> Class.instance_arity_cmd)
   6.607 -    >> (Toplevel.print oo Toplevel.theory_to_proof)
   6.608 -  || Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
   6.609 +  OuterSyntax.command "instance" "prove type arity or subclass relation" Keyword.thy_goal
   6.610 +  ((Parse.xname -- ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |-- Parse.!!! Parse.xname)
   6.611 +        >> Class.classrel_cmd ||
   6.612 +    Parse.multi_arity >> Class.instance_arity_cmd)
   6.613 +    >> (Toplevel.print oo Toplevel.theory_to_proof) ||
   6.614 +    Scan.succeed
   6.615 +      (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
   6.616  
   6.617  
   6.618  (* arbitrary overloading *)
   6.619  
   6.620  val _ =
   6.621 -  OuterSyntax.command "overloading" "overloaded definitions" K.thy_decl
   6.622 -   (Scan.repeat1 (P.name --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.term --
   6.623 -      Scan.optional (P.$$$ "(" |-- (P.$$$ "unchecked" >> K false) --| P.$$$ ")") true
   6.624 -      >> P.triple1) --| P.begin
   6.625 +  OuterSyntax.command "overloading" "overloaded definitions" Keyword.thy_decl
   6.626 +   (Scan.repeat1 (Parse.name --| (Parse.$$$ "\\<equiv>" || Parse.$$$ "==") -- Parse.term --
   6.627 +      Scan.optional (Parse.$$$ "(" |-- (Parse.$$$ "unchecked" >> K false) --| Parse.$$$ ")") true
   6.628 +      >> Parse.triple1) --| Parse.begin
   6.629     >> (fn operations => Toplevel.print o
   6.630           Toplevel.begin_local_theory true (Theory_Target.overloading_cmd operations)));
   6.631  
   6.632 @@ -486,8 +500,8 @@
   6.633  (* code generation *)
   6.634  
   6.635  val _ =
   6.636 -  OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl
   6.637 -    (Scan.repeat1 P.term >> (Toplevel.theory o Code.add_datatype_cmd));
   6.638 +  OuterSyntax.command "code_datatype" "define set of code datatype constructors" Keyword.thy_decl
   6.639 +    (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.add_datatype_cmd));
   6.640  
   6.641  
   6.642  
   6.643 @@ -499,7 +513,7 @@
   6.644    OuterSyntax.local_theory_to_proof'
   6.645      (if schematic then "schematic_" ^ kind else kind)
   6.646      ("state " ^ (if schematic then "schematic " ^ kind else kind))
   6.647 -    (if schematic then K.thy_schematic_goal else K.thy_goal)
   6.648 +    (if schematic then Keyword.thy_schematic_goal else Keyword.thy_goal)
   6.649      (Scan.optional (SpecParse.opt_thm_name ":" --|
   6.650        Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) Attrib.empty_binding --
   6.651        SpecParse.general_statement >> (fn (a, (elems, concl)) =>
   6.652 @@ -515,64 +529,64 @@
   6.653  
   6.654  val _ =
   6.655    OuterSyntax.local_theory_to_proof "example_proof"
   6.656 -    "example proof body, without any result" K.thy_schematic_goal
   6.657 +    "example proof body, without any result" Keyword.thy_schematic_goal
   6.658      (Scan.succeed
   6.659        (Specification.schematic_theorem_cmd "" NONE (K I)
   6.660          Attrib.empty_binding [] (Element.Shows []) false #> Proof.enter_forward));
   6.661  
   6.662  val _ =
   6.663    OuterSyntax.command "have" "state local goal"
   6.664 -    (K.tag_proof K.prf_goal)
   6.665 +    (Keyword.tag_proof Keyword.prf_goal)
   6.666      (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have));
   6.667  
   6.668  val _ =
   6.669    OuterSyntax.command "hence" "abbreviates \"then have\""
   6.670 -    (K.tag_proof K.prf_goal)
   6.671 +    (Keyword.tag_proof Keyword.prf_goal)
   6.672      (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.hence));
   6.673  
   6.674  val _ =
   6.675    OuterSyntax.command "show" "state local goal, solving current obligation"
   6.676 -    (K.tag_proof K.prf_asm_goal)
   6.677 +    (Keyword.tag_proof Keyword.prf_asm_goal)
   6.678      (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show));
   6.679  
   6.680  val _ =
   6.681    OuterSyntax.command "thus" "abbreviates \"then show\""
   6.682 -    (K.tag_proof K.prf_asm_goal)
   6.683 +    (Keyword.tag_proof Keyword.prf_asm_goal)
   6.684      (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus));
   6.685  
   6.686  
   6.687  (* facts *)
   6.688  
   6.689 -val facts = P.and_list1 SpecParse.xthms1;
   6.690 +val facts = Parse.and_list1 SpecParse.xthms1;
   6.691  
   6.692  val _ =
   6.693    OuterSyntax.command "then" "forward chaining"
   6.694 -    (K.tag_proof K.prf_chain)
   6.695 +    (Keyword.tag_proof Keyword.prf_chain)
   6.696      (Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain));
   6.697  
   6.698  val _ =
   6.699    OuterSyntax.command "from" "forward chaining from given facts"
   6.700 -    (K.tag_proof K.prf_chain)
   6.701 +    (Keyword.tag_proof Keyword.prf_chain)
   6.702      (facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss_cmd)));
   6.703  
   6.704  val _ =
   6.705    OuterSyntax.command "with" "forward chaining from given and current facts"
   6.706 -    (K.tag_proof K.prf_chain)
   6.707 +    (Keyword.tag_proof Keyword.prf_chain)
   6.708      (facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss_cmd)));
   6.709  
   6.710  val _ =
   6.711    OuterSyntax.command "note" "define facts"
   6.712 -    (K.tag_proof K.prf_decl)
   6.713 +    (Keyword.tag_proof Keyword.prf_decl)
   6.714      (SpecParse.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss_cmd)));
   6.715  
   6.716  val _ =
   6.717    OuterSyntax.command "using" "augment goal facts"
   6.718 -    (K.tag_proof K.prf_decl)
   6.719 +    (Keyword.tag_proof Keyword.prf_decl)
   6.720      (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using_cmd)));
   6.721  
   6.722  val _ =
   6.723    OuterSyntax.command "unfolding" "unfold definitions in goal and facts"
   6.724 -    (K.tag_proof K.prf_decl)
   6.725 +    (Keyword.tag_proof Keyword.prf_decl)
   6.726      (facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding_cmd)));
   6.727  
   6.728  
   6.729 @@ -580,57 +594,59 @@
   6.730  
   6.731  val _ =
   6.732    OuterSyntax.command "fix" "fix local variables (Skolem constants)"
   6.733 -    (K.tag_proof K.prf_asm)
   6.734 -    (P.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix_cmd)));
   6.735 +    (Keyword.tag_proof Keyword.prf_asm)
   6.736 +    (Parse.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix_cmd)));
   6.737  
   6.738  val _ =
   6.739    OuterSyntax.command "assume" "assume propositions"
   6.740 -    (K.tag_proof K.prf_asm)
   6.741 +    (Keyword.tag_proof Keyword.prf_asm)
   6.742      (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume_cmd)));
   6.743  
   6.744  val _ =
   6.745    OuterSyntax.command "presume" "assume propositions, to be established later"
   6.746 -    (K.tag_proof K.prf_asm)
   6.747 +    (Keyword.tag_proof Keyword.prf_asm)
   6.748      (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd)));
   6.749  
   6.750  val _ =
   6.751    OuterSyntax.command "def" "local definition"
   6.752 -    (K.tag_proof K.prf_asm)
   6.753 -    (P.and_list1
   6.754 +    (Keyword.tag_proof Keyword.prf_asm)
   6.755 +    (Parse.and_list1
   6.756        (SpecParse.opt_thm_name ":" --
   6.757 -        ((P.binding -- P.opt_mixfix) -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp)))
   6.758 +        ((Parse.binding -- Parse.opt_mixfix) --
   6.759 +          ((Parse.$$$ "\\<equiv>" || Parse.$$$ "==") |-- Parse.!!! Parse.termp)))
   6.760      >> (Toplevel.print oo (Toplevel.proof o Proof.def_cmd)));
   6.761  
   6.762  val _ =
   6.763    OuterSyntax.command "obtain" "generalized existence"
   6.764 -    (K.tag_proof K.prf_asm_goal)
   6.765 -    (P.parname -- Scan.optional (P.fixes --| P.where_) [] -- SpecParse.statement
   6.766 +    (Keyword.tag_proof Keyword.prf_asm_goal)
   6.767 +    (Parse.parname -- Scan.optional (Parse.fixes --| Parse.where_) [] -- SpecParse.statement
   6.768        >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain_cmd x y z)));
   6.769  
   6.770  val _ =
   6.771    OuterSyntax.command "guess" "wild guessing (unstructured)"
   6.772 -    (K.tag_proof K.prf_asm_goal)
   6.773 -    (Scan.optional P.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess_cmd)));
   6.774 +    (Keyword.tag_proof Keyword.prf_asm_goal)
   6.775 +    (Scan.optional Parse.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess_cmd)));
   6.776  
   6.777  val _ =
   6.778    OuterSyntax.command "let" "bind text variables"
   6.779 -    (K.tag_proof K.prf_decl)
   6.780 -    (P.and_list1 (P.and_list1 P.term -- (P.$$$ "=" |-- P.term))
   6.781 +    (Keyword.tag_proof Keyword.prf_decl)
   6.782 +    (Parse.and_list1 (Parse.and_list1 Parse.term -- (Parse.$$$ "=" |-- Parse.term))
   6.783        >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind_cmd)));
   6.784  
   6.785  val _ =
   6.786    OuterSyntax.command "write" "add concrete syntax for constants / fixed variables"
   6.787 -    (K.tag_proof K.prf_decl)
   6.788 -    (opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
   6.789 +    (Keyword.tag_proof Keyword.prf_decl)
   6.790 +    (opt_mode -- Parse.and_list1 (Parse.xname -- SpecParse.locale_mixfix)
   6.791      >> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args)));
   6.792  
   6.793  val case_spec =
   6.794 -  (P.$$$ "(" |-- P.!!! (P.xname -- Scan.repeat1 (P.maybe P.name) --| P.$$$ ")") ||
   6.795 -    P.xname >> rpair []) -- SpecParse.opt_attribs >> P.triple1;
   6.796 +  (Parse.$$$ "(" |--
   6.797 +    Parse.!!! (Parse.xname -- Scan.repeat1 (Parse.maybe Parse.name) --| Parse.$$$ ")") ||
   6.798 +    Parse.xname >> rpair []) -- SpecParse.opt_attribs >> Parse.triple1;
   6.799  
   6.800  val _ =
   6.801    OuterSyntax.command "case" "invoke local context"
   6.802 -    (K.tag_proof K.prf_asm)
   6.803 +    (Keyword.tag_proof Keyword.prf_asm)
   6.804      (case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case_cmd)));
   6.805  
   6.806  
   6.807 @@ -638,17 +654,17 @@
   6.808  
   6.809  val _ =
   6.810    OuterSyntax.command "{" "begin explicit proof block"
   6.811 -    (K.tag_proof K.prf_open)
   6.812 +    (Keyword.tag_proof Keyword.prf_open)
   6.813      (Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block));
   6.814  
   6.815  val _ =
   6.816    OuterSyntax.command "}" "end explicit proof block"
   6.817 -    (K.tag_proof K.prf_close)
   6.818 +    (Keyword.tag_proof Keyword.prf_close)
   6.819      (Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block));
   6.820  
   6.821  val _ =
   6.822    OuterSyntax.command "next" "enter next proof block"
   6.823 -    (K.tag_proof K.prf_block)
   6.824 +    (Keyword.tag_proof Keyword.prf_block)
   6.825      (Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block));
   6.826  
   6.827  
   6.828 @@ -656,37 +672,37 @@
   6.829  
   6.830  val _ =
   6.831    OuterSyntax.command "qed" "conclude (sub-)proof"
   6.832 -    (K.tag_proof K.qed_block)
   6.833 +    (Keyword.tag_proof Keyword.qed_block)
   6.834      (Scan.option Method.parse >> IsarCmd.qed);
   6.835  
   6.836  val _ =
   6.837    OuterSyntax.command "by" "terminal backward proof"
   6.838 -    (K.tag_proof K.qed)
   6.839 +    (Keyword.tag_proof Keyword.qed)
   6.840      (Method.parse -- Scan.option Method.parse >> IsarCmd.terminal_proof);
   6.841  
   6.842  val _ =
   6.843    OuterSyntax.command ".." "default proof"
   6.844 -    (K.tag_proof K.qed)
   6.845 +    (Keyword.tag_proof Keyword.qed)
   6.846      (Scan.succeed IsarCmd.default_proof);
   6.847  
   6.848  val _ =
   6.849    OuterSyntax.command "." "immediate proof"
   6.850 -    (K.tag_proof K.qed)
   6.851 +    (Keyword.tag_proof Keyword.qed)
   6.852      (Scan.succeed IsarCmd.immediate_proof);
   6.853  
   6.854  val _ =
   6.855    OuterSyntax.command "done" "done proof"
   6.856 -    (K.tag_proof K.qed)
   6.857 +    (Keyword.tag_proof Keyword.qed)
   6.858      (Scan.succeed IsarCmd.done_proof);
   6.859  
   6.860  val _ =
   6.861    OuterSyntax.command "sorry" "skip proof (quick-and-dirty mode only!)"
   6.862 -    (K.tag_proof K.qed)
   6.863 +    (Keyword.tag_proof Keyword.qed)
   6.864      (Scan.succeed IsarCmd.skip_proof);
   6.865  
   6.866  val _ =
   6.867    OuterSyntax.command "oops" "forget proof"
   6.868 -    (K.tag_proof K.qed_global)
   6.869 +    (Keyword.tag_proof Keyword.qed_global)
   6.870      (Scan.succeed Toplevel.forget_proof);
   6.871  
   6.872  
   6.873 @@ -694,27 +710,27 @@
   6.874  
   6.875  val _ =
   6.876    OuterSyntax.command "defer" "shuffle internal proof state"
   6.877 -    (K.tag_proof K.prf_script)
   6.878 -    (Scan.option P.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.defer)));
   6.879 +    (Keyword.tag_proof Keyword.prf_script)
   6.880 +    (Scan.option Parse.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.defer)));
   6.881  
   6.882  val _ =
   6.883    OuterSyntax.command "prefer" "shuffle internal proof state"
   6.884 -    (K.tag_proof K.prf_script)
   6.885 -    (P.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.prefer)));
   6.886 +    (Keyword.tag_proof Keyword.prf_script)
   6.887 +    (Parse.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.prefer)));
   6.888  
   6.889  val _ =
   6.890    OuterSyntax.command "apply" "initial refinement step (unstructured)"
   6.891 -    (K.tag_proof K.prf_script)
   6.892 +    (Keyword.tag_proof Keyword.prf_script)
   6.893      (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply)));
   6.894  
   6.895  val _ =
   6.896    OuterSyntax.command "apply_end" "terminal refinement (unstructured)"
   6.897 -    (K.tag_proof K.prf_script)
   6.898 +    (Keyword.tag_proof Keyword.prf_script)
   6.899      (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end)));
   6.900  
   6.901  val _ =
   6.902    OuterSyntax.command "proof" "backward proof"
   6.903 -    (K.tag_proof K.prf_block)
   6.904 +    (Keyword.tag_proof Keyword.prf_block)
   6.905      (Scan.option Method.parse >> (fn m => Toplevel.print o
   6.906        Toplevel.actual_proof (Proof_Node.applys (Proof.proof m)) o
   6.907        Toplevel.skip_proof (fn i => i + 1)));
   6.908 @@ -723,26 +739,26 @@
   6.909  (* calculational proof commands *)
   6.910  
   6.911  val calc_args =
   6.912 -  Scan.option (P.$$$ "(" |-- P.!!! ((SpecParse.xthms1 --| P.$$$ ")")));
   6.913 +  Scan.option (Parse.$$$ "(" |-- Parse.!!! ((SpecParse.xthms1 --| Parse.$$$ ")")));
   6.914  
   6.915  val _ =
   6.916    OuterSyntax.command "also" "combine calculation and current facts"
   6.917 -    (K.tag_proof K.prf_decl)
   6.918 +    (Keyword.tag_proof Keyword.prf_decl)
   6.919      (calc_args >> (Toplevel.proofs' o Calculation.also_cmd));
   6.920  
   6.921  val _ =
   6.922    OuterSyntax.command "finally" "combine calculation and current facts, exhibit result"
   6.923 -    (K.tag_proof K.prf_chain)
   6.924 +    (Keyword.tag_proof Keyword.prf_chain)
   6.925      (calc_args >> (Toplevel.proofs' o Calculation.finally_cmd));
   6.926  
   6.927  val _ =
   6.928    OuterSyntax.command "moreover" "augment calculation by current facts"
   6.929 -    (K.tag_proof K.prf_decl)
   6.930 +    (Keyword.tag_proof Keyword.prf_decl)
   6.931      (Scan.succeed (Toplevel.proof' Calculation.moreover));
   6.932  
   6.933  val _ =
   6.934    OuterSyntax.command "ultimately" "augment calculation by current facts, exhibit result"
   6.935 -    (K.tag_proof K.prf_chain)
   6.936 +    (Keyword.tag_proof Keyword.prf_chain)
   6.937      (Scan.succeed (Toplevel.proof' Calculation.ultimately));
   6.938  
   6.939  
   6.940 @@ -750,18 +766,19 @@
   6.941  
   6.942  val _ =
   6.943    OuterSyntax.command "back" "backtracking of proof command"
   6.944 -    (K.tag_proof K.prf_script)
   6.945 +    (Keyword.tag_proof Keyword.prf_script)
   6.946      (Scan.succeed (Toplevel.print o Toplevel.actual_proof Proof_Node.back o Toplevel.skip_proof I));
   6.947  
   6.948  
   6.949  (* nested commands *)
   6.950  
   6.951  val props_text =
   6.952 -  Scan.optional ValueParse.properties [] -- P.position P.string >> (fn (props, (str, pos)) =>
   6.953 -    (Position.of_properties (Position.default_properties pos props), str));
   6.954 +  Scan.optional ValueParse.properties [] -- Parse.position Parse.string
   6.955 +  >> (fn (props, (str, pos)) =>
   6.956 +      (Position.of_properties (Position.default_properties pos props), str));
   6.957  
   6.958  val _ =
   6.959 -  OuterSyntax.improper_command "Isabelle.command" "nested Isabelle command" K.control
   6.960 +  OuterSyntax.improper_command "Isabelle.command" "nested Isabelle command" Keyword.control
   6.961      (props_text :|-- (fn (pos, str) =>
   6.962        (case OuterSyntax.parse pos str of
   6.963          [tr] => Scan.succeed (K tr)
   6.964 @@ -772,151 +789,153 @@
   6.965  
   6.966  (** diagnostic commands (for interactive mode only) **)
   6.967  
   6.968 -val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
   6.969 -val opt_bang = Scan.optional (P.$$$ "!" >> K true) false;
   6.970 +val opt_modes =
   6.971 +  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
   6.972 +
   6.973 +val opt_bang = Scan.optional (Parse.$$$ "!" >> K true) false;
   6.974  
   6.975  val _ =
   6.976    OuterSyntax.improper_command "pretty_setmargin" "change default margin for pretty printing"
   6.977 -    K.diag (P.nat >> (Toplevel.no_timing oo IsarCmd.pretty_setmargin));
   6.978 +    Keyword.diag (Parse.nat >> (Toplevel.no_timing oo IsarCmd.pretty_setmargin));
   6.979  
   6.980  val _ =
   6.981 -  OuterSyntax.improper_command "help" "print outer syntax commands" K.diag
   6.982 +  OuterSyntax.improper_command "help" "print outer syntax commands" Keyword.diag
   6.983      (Scan.succeed (Toplevel.no_timing o Toplevel.imperative OuterSyntax.print_outer_syntax));
   6.984  
   6.985  val _ =
   6.986 -  OuterSyntax.improper_command "print_commands" "print outer syntax commands" K.diag
   6.987 +  OuterSyntax.improper_command "print_commands" "print outer syntax commands" Keyword.diag
   6.988      (Scan.succeed (Toplevel.no_timing o Toplevel.imperative OuterSyntax.print_outer_syntax));
   6.989  
   6.990  val _ =
   6.991 -  OuterSyntax.improper_command "print_configs" "print configuration options" K.diag
   6.992 +  OuterSyntax.improper_command "print_configs" "print configuration options" Keyword.diag
   6.993      (Scan.succeed (Toplevel.no_timing o IsarCmd.print_configs));
   6.994  
   6.995  val _ =
   6.996 -  OuterSyntax.improper_command "print_context" "print theory context name" K.diag
   6.997 +  OuterSyntax.improper_command "print_context" "print theory context name" Keyword.diag
   6.998      (Scan.succeed (Toplevel.no_timing o IsarCmd.print_context));
   6.999  
  6.1000  val _ =
  6.1001 -  OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag
  6.1002 -    (opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theory));
  6.1003 +  OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)"
  6.1004 +    Keyword.diag (opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theory));
  6.1005  
  6.1006  val _ =
  6.1007 -  OuterSyntax.improper_command "print_syntax" "print inner syntax of context (verbose!)" K.diag
  6.1008 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax));
  6.1009 +  OuterSyntax.improper_command "print_syntax" "print inner syntax of context (verbose!)"
  6.1010 +    Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax));
  6.1011  
  6.1012  val _ =
  6.1013 -  OuterSyntax.improper_command "print_abbrevs" "print constant abbreviation of context" K.diag
  6.1014 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_abbrevs));
  6.1015 +  OuterSyntax.improper_command "print_abbrevs" "print constant abbreviation of context"
  6.1016 +    Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.print_abbrevs));
  6.1017  
  6.1018  val _ =
  6.1019    OuterSyntax.improper_command "print_theorems"
  6.1020 -      "print theorems of local theory or proof context" K.diag
  6.1021 +      "print theorems of local theory or proof context" Keyword.diag
  6.1022      (opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theorems));
  6.1023  
  6.1024  val _ =
  6.1025 -  OuterSyntax.improper_command "print_locales" "print locales of this theory" K.diag
  6.1026 +  OuterSyntax.improper_command "print_locales" "print locales of this theory" Keyword.diag
  6.1027      (Scan.succeed (Toplevel.no_timing o IsarCmd.print_locales));
  6.1028  
  6.1029  val _ =
  6.1030 -  OuterSyntax.improper_command "print_classes" "print classes of this theory" K.diag
  6.1031 +  OuterSyntax.improper_command "print_classes" "print classes of this theory" Keyword.diag
  6.1032      (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory
  6.1033        o Toplevel.keep (Class.print_classes o Toplevel.theory_of)));
  6.1034  
  6.1035  val _ =
  6.1036 -  OuterSyntax.improper_command "print_locale" "print locale of this theory" K.diag
  6.1037 -    (opt_bang -- P.xname >> (Toplevel.no_timing oo IsarCmd.print_locale));
  6.1038 +  OuterSyntax.improper_command "print_locale" "print locale of this theory" Keyword.diag
  6.1039 +    (opt_bang -- Parse.xname >> (Toplevel.no_timing oo IsarCmd.print_locale));
  6.1040  
  6.1041  val _ =
  6.1042    OuterSyntax.improper_command "print_interps"
  6.1043 -    "print interpretations of locale for this theory" K.diag
  6.1044 -    (P.xname >> (Toplevel.no_timing oo IsarCmd.print_registrations));
  6.1045 +    "print interpretations of locale for this theory" Keyword.diag
  6.1046 +    (Parse.xname >> (Toplevel.no_timing oo IsarCmd.print_registrations));
  6.1047  
  6.1048  val _ =
  6.1049 -  OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag
  6.1050 +  OuterSyntax.improper_command "print_attributes" "print attributes of this theory" Keyword.diag
  6.1051      (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes));
  6.1052  
  6.1053  val _ =
  6.1054 -  OuterSyntax.improper_command "print_simpset" "print context of Simplifier" K.diag
  6.1055 +  OuterSyntax.improper_command "print_simpset" "print context of Simplifier" Keyword.diag
  6.1056      (Scan.succeed (Toplevel.no_timing o IsarCmd.print_simpset));
  6.1057  
  6.1058  val _ =
  6.1059 -  OuterSyntax.improper_command "print_rules" "print intro/elim rules" K.diag
  6.1060 +  OuterSyntax.improper_command "print_rules" "print intro/elim rules" Keyword.diag
  6.1061      (Scan.succeed (Toplevel.no_timing o IsarCmd.print_rules));
  6.1062  
  6.1063  val _ =
  6.1064 -  OuterSyntax.improper_command "print_trans_rules" "print transitivity rules" K.diag
  6.1065 +  OuterSyntax.improper_command "print_trans_rules" "print transitivity rules" Keyword.diag
  6.1066      (Scan.succeed (Toplevel.no_timing o IsarCmd.print_trans_rules));
  6.1067  
  6.1068  val _ =
  6.1069 -  OuterSyntax.improper_command "print_methods" "print methods of this theory" K.diag
  6.1070 +  OuterSyntax.improper_command "print_methods" "print methods of this theory" Keyword.diag
  6.1071      (Scan.succeed (Toplevel.no_timing o IsarCmd.print_methods));
  6.1072  
  6.1073  val _ =
  6.1074 -  OuterSyntax.improper_command "print_antiquotations" "print antiquotations (global)" K.diag
  6.1075 +  OuterSyntax.improper_command "print_antiquotations" "print antiquotations (global)" Keyword.diag
  6.1076      (Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations));
  6.1077  
  6.1078  val _ =
  6.1079    OuterSyntax.improper_command "thy_deps" "visualize theory dependencies"
  6.1080 -    K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.thy_deps));
  6.1081 +    Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.thy_deps));
  6.1082  
  6.1083  val _ =
  6.1084    OuterSyntax.improper_command "class_deps" "visualize class dependencies"
  6.1085 -    K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.class_deps));
  6.1086 +    Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.class_deps));
  6.1087  
  6.1088  val _ =
  6.1089    OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies"
  6.1090 -    K.diag (SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
  6.1091 +    Keyword.diag (SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
  6.1092  
  6.1093  val _ =
  6.1094 -  OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag
  6.1095 +  OuterSyntax.improper_command "print_binds" "print term bindings of proof context" Keyword.diag
  6.1096      (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds));
  6.1097  
  6.1098  val _ =
  6.1099 -  OuterSyntax.improper_command "print_facts" "print facts of proof context" K.diag
  6.1100 +  OuterSyntax.improper_command "print_facts" "print facts of proof context" Keyword.diag
  6.1101      (Scan.succeed (Toplevel.no_timing o IsarCmd.print_facts));
  6.1102  
  6.1103  val _ =
  6.1104 -  OuterSyntax.improper_command "print_cases" "print cases of proof context" K.diag
  6.1105 +  OuterSyntax.improper_command "print_cases" "print cases of proof context" Keyword.diag
  6.1106      (Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases));
  6.1107  
  6.1108  val _ =
  6.1109 -  OuterSyntax.improper_command "print_statement" "print theorems as long statements" K.diag
  6.1110 +  OuterSyntax.improper_command "print_statement" "print theorems as long statements" Keyword.diag
  6.1111      (opt_modes -- SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts));
  6.1112  
  6.1113  val _ =
  6.1114 -  OuterSyntax.improper_command "thm" "print theorems" K.diag
  6.1115 +  OuterSyntax.improper_command "thm" "print theorems" Keyword.diag
  6.1116      (opt_modes -- SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms));
  6.1117  
  6.1118  val _ =
  6.1119 -  OuterSyntax.improper_command "prf" "print proof terms of theorems" K.diag
  6.1120 +  OuterSyntax.improper_command "prf" "print proof terms of theorems" Keyword.diag
  6.1121      (opt_modes -- Scan.option SpecParse.xthms1
  6.1122        >> (Toplevel.no_timing oo IsarCmd.print_prfs false));
  6.1123  
  6.1124  val _ =
  6.1125 -  OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" K.diag
  6.1126 +  OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" Keyword.diag
  6.1127      (opt_modes -- Scan.option SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs true));
  6.1128  
  6.1129  val _ =
  6.1130 -  OuterSyntax.improper_command "prop" "read and print proposition" K.diag
  6.1131 -    (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_prop));
  6.1132 +  OuterSyntax.improper_command "prop" "read and print proposition" Keyword.diag
  6.1133 +    (opt_modes -- Parse.term >> (Toplevel.no_timing oo IsarCmd.print_prop));
  6.1134  
  6.1135  val _ =
  6.1136 -  OuterSyntax.improper_command "term" "read and print term" K.diag
  6.1137 -    (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_term));
  6.1138 +  OuterSyntax.improper_command "term" "read and print term" Keyword.diag
  6.1139 +    (opt_modes -- Parse.term >> (Toplevel.no_timing oo IsarCmd.print_term));
  6.1140  
  6.1141  val _ =
  6.1142 -  OuterSyntax.improper_command "typ" "read and print type" K.diag
  6.1143 -    (opt_modes -- P.typ >> (Toplevel.no_timing oo IsarCmd.print_type));
  6.1144 +  OuterSyntax.improper_command "typ" "read and print type" Keyword.diag
  6.1145 +    (opt_modes -- Parse.typ >> (Toplevel.no_timing oo IsarCmd.print_type));
  6.1146  
  6.1147  val _ =
  6.1148 -  OuterSyntax.improper_command "print_codesetup" "print code generator setup" K.diag
  6.1149 +  OuterSyntax.improper_command "print_codesetup" "print code generator setup" Keyword.diag
  6.1150      (Scan.succeed
  6.1151        (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
  6.1152          (Code.print_codesetup o Toplevel.theory_of)));
  6.1153  
  6.1154  val _ =
  6.1155 -  OuterSyntax.improper_command "unused_thms" "find unused theorems" K.diag
  6.1156 -    (Scan.option ((Scan.repeat1 (Scan.unless P.minus P.name) --| P.minus) --
  6.1157 -       Scan.option (Scan.repeat1 (Scan.unless P.minus P.name))) >>
  6.1158 +  OuterSyntax.improper_command "unused_thms" "find unused theorems" Keyword.diag
  6.1159 +    (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
  6.1160 +       Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >>
  6.1161           (Toplevel.no_timing oo IsarCmd.unused_thms));
  6.1162  
  6.1163  
  6.1164 @@ -924,66 +943,66 @@
  6.1165  (** system commands (for interactive mode only) **)
  6.1166  
  6.1167  val _ =
  6.1168 -  OuterSyntax.improper_command "cd" "change current working directory" K.diag
  6.1169 -    (P.path >> (Toplevel.no_timing oo IsarCmd.cd));
  6.1170 +  OuterSyntax.improper_command "cd" "change current working directory" Keyword.diag
  6.1171 +    (Parse.path >> (Toplevel.no_timing oo IsarCmd.cd));
  6.1172  
  6.1173  val _ =
  6.1174 -  OuterSyntax.improper_command "pwd" "print current working directory" K.diag
  6.1175 +  OuterSyntax.improper_command "pwd" "print current working directory" Keyword.diag
  6.1176      (Scan.succeed (Toplevel.no_timing o IsarCmd.pwd));
  6.1177  
  6.1178  val _ =
  6.1179 -  OuterSyntax.improper_command "use_thy" "use theory file" K.diag
  6.1180 -    (P.name >> (fn name =>
  6.1181 +  OuterSyntax.improper_command "use_thy" "use theory file" Keyword.diag
  6.1182 +    (Parse.name >> (fn name =>
  6.1183        Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.use_thy name)));
  6.1184  
  6.1185  val _ =
  6.1186 -  OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag
  6.1187 -    (P.name >> (fn name =>
  6.1188 +  OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" Keyword.diag
  6.1189 +    (Parse.name >> (fn name =>
  6.1190        Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.touch_thy name)));
  6.1191  
  6.1192  val _ =
  6.1193 -  OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag
  6.1194 -    (P.name >> (fn name =>
  6.1195 +  OuterSyntax.improper_command "remove_thy" "remove theory from loader database" Keyword.diag
  6.1196 +    (Parse.name >> (fn name =>
  6.1197        Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.remove_thy name)));
  6.1198  
  6.1199  val _ =
  6.1200    OuterSyntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"
  6.1201 -    K.diag (P.name >> (fn name =>
  6.1202 +    Keyword.diag (Parse.name >> (fn name =>
  6.1203        Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.kill_thy name)));
  6.1204  
  6.1205  val _ =
  6.1206    OuterSyntax.improper_command "display_drafts" "display raw source files with symbols"
  6.1207 -    K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.display_drafts));
  6.1208 +    Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo IsarCmd.display_drafts));
  6.1209  
  6.1210  val _ =
  6.1211    OuterSyntax.improper_command "print_drafts" "print raw source files with symbols"
  6.1212 -    K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.print_drafts));
  6.1213 +    Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo IsarCmd.print_drafts));
  6.1214  
  6.1215  val opt_limits =
  6.1216 -  Scan.option P.nat -- Scan.option (P.$$$ "," |-- P.!!! P.nat);
  6.1217 +  Scan.option Parse.nat -- Scan.option (Parse.$$$ "," |-- Parse.!!! Parse.nat);
  6.1218  
  6.1219  val _ =
  6.1220 -  OuterSyntax.improper_command "pr" "print current proof state (if present)" K.diag
  6.1221 +  OuterSyntax.improper_command "pr" "print current proof state (if present)" Keyword.diag
  6.1222      (opt_modes -- opt_limits >> (Toplevel.no_timing oo IsarCmd.pr));
  6.1223  
  6.1224  val _ =
  6.1225 -  OuterSyntax.improper_command "disable_pr" "disable printing of toplevel state" K.diag
  6.1226 +  OuterSyntax.improper_command "disable_pr" "disable printing of toplevel state" Keyword.diag
  6.1227      (Scan.succeed (Toplevel.no_timing o IsarCmd.disable_pr));
  6.1228  
  6.1229  val _ =
  6.1230 -  OuterSyntax.improper_command "enable_pr" "enable printing of toplevel state" K.diag
  6.1231 +  OuterSyntax.improper_command "enable_pr" "enable printing of toplevel state" Keyword.diag
  6.1232      (Scan.succeed (Toplevel.no_timing o IsarCmd.enable_pr));
  6.1233  
  6.1234  val _ =
  6.1235 -  OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag
  6.1236 -    (P.opt_unit >> K (Toplevel.no_timing o Toplevel.imperative Secure.commit));
  6.1237 +  OuterSyntax.improper_command "commit" "commit current session to ML database" Keyword.diag
  6.1238 +    (Parse.opt_unit >> K (Toplevel.no_timing o Toplevel.imperative Secure.commit));
  6.1239  
  6.1240  val _ =
  6.1241 -  OuterSyntax.improper_command "quit" "quit Isabelle" K.control
  6.1242 -    (P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit));
  6.1243 +  OuterSyntax.improper_command "quit" "quit Isabelle" Keyword.control
  6.1244 +    (Parse.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit));
  6.1245  
  6.1246  val _ =
  6.1247 -  OuterSyntax.improper_command "exit" "exit Isar loop" K.control
  6.1248 +  OuterSyntax.improper_command "exit" "exit Isar loop" Keyword.control
  6.1249      (Scan.succeed (Toplevel.no_timing o IsarCmd.exit));
  6.1250  
  6.1251  end;
     7.1 --- a/src/Pure/Isar/method.ML	Sat May 15 22:24:25 2010 +0200
     7.2 +++ b/src/Pure/Isar/method.ML	Sat May 15 23:16:32 2010 +0200
     7.3 @@ -382,9 +382,6 @@
     7.4  
     7.5  (** concrete syntax **)
     7.6  
     7.7 -structure P = OuterParse;
     7.8 -
     7.9 -
    7.10  (* sections *)
    7.11  
    7.12  type modifier = (Proof.context -> Proof.context) * attribute;
    7.13 @@ -407,7 +404,7 @@
    7.14  (* extra rule methods *)
    7.15  
    7.16  fun xrule_meth m =
    7.17 -  Scan.lift (Scan.optional (Args.parens OuterParse.nat) 0) -- Attrib.thms >>
    7.18 +  Scan.lift (Scan.optional (Args.parens Parse.nat) 0) -- Attrib.thms >>
    7.19    (fn (n, ths) => K (m n ths));
    7.20  
    7.21  
    7.22 @@ -419,18 +416,18 @@
    7.23  local
    7.24  
    7.25  fun meth4 x =
    7.26 - (P.position (P.xname >> rpair []) >> (Source o Args.src) ||
    7.27 -  P.$$$ "(" |-- P.!!! (meth0 --| P.$$$ ")")) x
    7.28 + (Parse.position (Parse.xname >> rpair []) >> (Source o Args.src) ||
    7.29 +  Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x
    7.30  and meth3 x =
    7.31 - (meth4 --| P.$$$ "?" >> Try ||
    7.32 -  meth4 --| P.$$$ "+" >> Repeat1 ||
    7.33 -  meth4 -- (P.$$$ "[" |-- Scan.optional P.nat 1 --| P.$$$ "]") >> (SelectGoals o swap) ||
    7.34 + (meth4 --| Parse.$$$ "?" >> Try ||
    7.35 +  meth4 --| Parse.$$$ "+" >> Repeat1 ||
    7.36 +  meth4 -- (Parse.$$$ "[" |-- Scan.optional Parse.nat 1 --| Parse.$$$ "]") >> (SelectGoals o swap) ||
    7.37    meth4) x
    7.38  and meth2 x =
    7.39 - (P.position (P.xname -- Args.parse1 is_symid_meth) >> (Source o Args.src) ||
    7.40 + (Parse.position (Parse.xname -- Args.parse1 is_symid_meth) >> (Source o Args.src) ||
    7.41    meth3) x
    7.42 -and meth1 x = (P.enum1 "," meth2 >> (fn [m] => m | ms => Then ms)) x
    7.43 -and meth0 x = (P.enum1 "|" meth1 >> (fn [m] => m | ms => Orelse ms)) x;
    7.44 +and meth1 x = (Parse.enum1 "," meth2 >> (fn [m] => m | ms => Then ms)) x
    7.45 +and meth0 x = (Parse.enum1 "|" meth1 >> (fn [m] => m | ms => Orelse ms)) x;
    7.46  
    7.47  in val parse = meth3 end;
    7.48  
    7.49 @@ -463,12 +460,12 @@
    7.50    setup (Binding.name "rename_tac") (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name) >>
    7.51      (fn (quant, xs) => K (SIMPLE_METHOD'' quant (Tactic.rename_tac xs))))
    7.52      "rename parameters of goal" #>
    7.53 -  setup (Binding.name "rotate_tac") (Args.goal_spec -- Scan.lift (Scan.optional P.int 1) >>
    7.54 +  setup (Binding.name "rotate_tac") (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >>
    7.55      (fn (quant, i) => K (SIMPLE_METHOD'' quant (Tactic.rotate_tac i))))
    7.56        "rotate assumptions of goal" #>
    7.57 -  setup (Binding.name "tactic") (Scan.lift (P.position Args.name) >> tactic)
    7.58 +  setup (Binding.name "tactic") (Scan.lift (Parse.position Args.name) >> tactic)
    7.59      "ML tactic as proof method" #>
    7.60 -  setup (Binding.name "raw_tactic") (Scan.lift (P.position Args.name) >> raw_tactic)
    7.61 +  setup (Binding.name "raw_tactic") (Scan.lift (Parse.position Args.name) >> raw_tactic)
    7.62      "ML tactic as raw proof method"));
    7.63  
    7.64  
     8.1 --- a/src/Pure/Isar/outer_syntax.ML	Sat May 15 22:24:25 2010 +0200
     8.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sat May 15 23:16:32 2010 +0200
     8.3 @@ -9,20 +9,20 @@
     8.4  
     8.5  signature OUTER_SYNTAX =
     8.6  sig
     8.7 -  val command: string -> string -> OuterKeyword.T ->
     8.8 +  val command: string -> string -> Keyword.T ->
     8.9      (Toplevel.transition -> Toplevel.transition) parser -> unit
    8.10 -  val markup_command: ThyOutput.markup -> string -> string -> OuterKeyword.T ->
    8.11 +  val markup_command: ThyOutput.markup -> string -> string -> Keyword.T ->
    8.12      (Toplevel.transition -> Toplevel.transition) parser -> unit
    8.13 -  val improper_command: string -> string -> OuterKeyword.T ->
    8.14 +  val improper_command: string -> string -> Keyword.T ->
    8.15      (Toplevel.transition -> Toplevel.transition) parser -> unit
    8.16    val internal_command: string -> (Toplevel.transition -> Toplevel.transition) parser -> unit
    8.17 -  val local_theory': string -> string -> OuterKeyword.T ->
    8.18 +  val local_theory': string -> string -> Keyword.T ->
    8.19      (bool -> local_theory -> local_theory) parser -> unit
    8.20 -  val local_theory: string -> string -> OuterKeyword.T ->
    8.21 +  val local_theory: string -> string -> Keyword.T ->
    8.22      (local_theory -> local_theory) parser -> unit
    8.23 -  val local_theory_to_proof': string -> string -> OuterKeyword.T ->
    8.24 +  val local_theory_to_proof': string -> string -> Keyword.T ->
    8.25      (bool -> local_theory -> Proof.state) parser -> unit
    8.26 -  val local_theory_to_proof: string -> string -> OuterKeyword.T ->
    8.27 +  val local_theory_to_proof: string -> string -> Keyword.T ->
    8.28      (local_theory -> Proof.state) parser -> unit
    8.29    val print_outer_syntax: unit -> unit
    8.30    val scan: Position.T -> string -> OuterLex.token list
    8.31 @@ -38,8 +38,7 @@
    8.32  struct
    8.33  
    8.34  structure T = OuterLex;
    8.35 -structure P = OuterParse;
    8.36 -type 'a parser = 'a P.parser;
    8.37 +type 'a parser = 'a Parse.parser;
    8.38  
    8.39  
    8.40  
    8.41 @@ -62,20 +61,20 @@
    8.42  local
    8.43  
    8.44  fun terminate false = Scan.succeed ()
    8.45 -  | terminate true = P.group "end of input" (Scan.option P.sync -- P.semicolon >> K ());
    8.46 +  | terminate true = Parse.group "end of input" (Scan.option Parse.sync -- Parse.semicolon >> K ());
    8.47  
    8.48  fun body cmd (name, _) =
    8.49    (case cmd name of
    8.50      SOME (Command {int_only, parse, ...}) =>
    8.51 -      P.!!! (Scan.prompt (name ^ "# ") (P.tags |-- parse >> pair int_only))
    8.52 +      Parse.!!! (Scan.prompt (name ^ "# ") (Parse.tags |-- parse >> pair int_only))
    8.53    | NONE => sys_error ("no parser for outer syntax command " ^ quote name));
    8.54  
    8.55  in
    8.56  
    8.57  fun parse_command do_terminate cmd =
    8.58 -  P.semicolon >> K NONE ||
    8.59 -  P.sync >> K NONE ||
    8.60 -  (P.position P.command :-- body cmd) --| terminate do_terminate
    8.61 +  Parse.semicolon >> K NONE ||
    8.62 +  Parse.sync >> K NONE ||
    8.63 +  (Parse.position Parse.command :-- body cmd) --| terminate do_terminate
    8.64      >> (fn ((name, pos), (int_only, f)) =>
    8.65        SOME (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |>
    8.66          Toplevel.interactive int_only |> f));
    8.67 @@ -105,7 +104,7 @@
    8.68  fun get_markups () = ! global_markups;
    8.69  
    8.70  fun get_command () = Symtab.lookup (get_commands ());
    8.71 -fun get_syntax () = CRITICAL (fn () => (OuterKeyword.get_lexicons (), get_command ()));
    8.72 +fun get_syntax () = CRITICAL (fn () => (Keyword.get_lexicons (), get_command ()));
    8.73  
    8.74  fun is_markup kind name = AList.lookup (op =) (get_markups ()) name = SOME kind;
    8.75  
    8.76 @@ -113,7 +112,7 @@
    8.77  (* augment syntax *)
    8.78  
    8.79  fun add_command name kind cmd = CRITICAL (fn () =>
    8.80 - (OuterKeyword.command name kind;
    8.81 + (Keyword.command name kind;
    8.82    if not (Symtab.defined (get_commands ()) name) then ()
    8.83    else warning ("Redefining outer syntax command " ^ quote name);
    8.84    change_commands (Symtab.update (name, cmd))));
    8.85 @@ -130,13 +129,13 @@
    8.86  end;
    8.87  
    8.88  fun internal_command name parse =
    8.89 -  command name "(internal)" OuterKeyword.control (parse >> (fn tr => Toplevel.no_timing o tr));
    8.90 +  command name "(internal)" Keyword.control (parse >> (fn tr => Toplevel.no_timing o tr));
    8.91  
    8.92  
    8.93  (* local_theory commands *)
    8.94  
    8.95  fun local_theory_command do_print trans name comment kind parse =
    8.96 -  command name comment kind (P.opt_target -- parse
    8.97 +  command name comment kind (Parse.opt_target -- parse
    8.98      >> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f));
    8.99  
   8.100  val local_theory' = local_theory_command false Toplevel.local_theory';
   8.101 @@ -157,7 +156,7 @@
   8.102        Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
   8.103      val (int_cmds, cmds) = List.partition #3 (dest_commands ());
   8.104    in
   8.105 -    [Pretty.strs ("syntax keywords:" :: map quote (OuterKeyword.dest_keywords ())),
   8.106 +    [Pretty.strs ("syntax keywords:" :: map quote (Keyword.dest_keywords ())),
   8.107        Pretty.big_list "commands:" (map pretty_cmd cmds),
   8.108        Pretty.big_list "interactive-only commands:" (map pretty_cmd int_cmds)]
   8.109      |> Pretty.chunks |> Pretty.writeln
   8.110 @@ -172,18 +171,18 @@
   8.111  fun toplevel_source term do_recover cmd src =
   8.112    let
   8.113      val no_terminator =
   8.114 -      Scan.unless P.semicolon (Scan.one (T.not_sync andf T.not_eof));
   8.115 +      Scan.unless Parse.semicolon (Scan.one (T.not_sync andf T.not_eof));
   8.116      fun recover int =
   8.117        (int, fn _ => Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]);
   8.118    in
   8.119      src
   8.120      |> T.source_proper
   8.121      |> Source.source T.stopper
   8.122 -      (Scan.bulk (P.$$$ "--" -- P.!!! P.doc_source >> K NONE || P.not_eof >> SOME))
   8.123 +      (Scan.bulk (Parse.$$$ "--" -- Parse.!!! Parse.doc_source >> K NONE || Parse.not_eof >> SOME))
   8.124          (Option.map recover do_recover)
   8.125      |> Source.map_filter I
   8.126      |> Source.source T.stopper
   8.127 -        (Scan.bulk (fn xs => P.!!! (parse_command term (cmd ())) xs))
   8.128 +        (Scan.bulk (fn xs => Parse.!!! (parse_command term (cmd ())) xs))
   8.129          (Option.map recover do_recover)
   8.130      |> Source.map_filter I
   8.131    end;
   8.132 @@ -194,13 +193,13 @@
   8.133  fun scan pos str =
   8.134    Source.of_string str
   8.135    |> Symbol.source {do_recover = false}
   8.136 -  |> T.source {do_recover = SOME false} OuterKeyword.get_lexicons pos
   8.137 +  |> T.source {do_recover = SOME false} Keyword.get_lexicons pos
   8.138    |> Source.exhaust;
   8.139  
   8.140  fun parse pos str =
   8.141    Source.of_string str
   8.142    |> Symbol.source {do_recover = false}
   8.143 -  |> T.source {do_recover = SOME false} OuterKeyword.get_lexicons pos
   8.144 +  |> T.source {do_recover = SOME false} Keyword.get_lexicons pos
   8.145    |> toplevel_source false NONE get_command
   8.146    |> Source.exhaust;
   8.147  
   8.148 @@ -231,7 +230,7 @@
   8.149  fun isar term : isar =
   8.150    Source.tty
   8.151    |> Symbol.source {do_recover = true}
   8.152 -  |> T.source {do_recover = SOME true} OuterKeyword.get_lexicons Position.none
   8.153 +  |> T.source {do_recover = SOME true} Keyword.get_lexicons Position.none
   8.154    |> toplevel_source term (SOME true) get_command;
   8.155  
   8.156  
   8.157 @@ -291,7 +290,7 @@
   8.158      val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
   8.159  
   8.160      fun after_load () =
   8.161 -      ThyOutput.present_thy (#1 lexs) OuterKeyword.command_tags is_markup (Lazy.force results) toks
   8.162 +      ThyOutput.present_thy (#1 lexs) Keyword.command_tags is_markup (Lazy.force results) toks
   8.163        |> Buffer.content
   8.164        |> Present.theory_output name;
   8.165    in after_load end;
     9.1 --- a/src/Pure/Isar/rule_insts.ML	Sat May 15 22:24:25 2010 +0200
     9.2 +++ b/src/Pure/Isar/rule_insts.ML	Sat May 15 23:16:32 2010 +0200
     9.3 @@ -30,7 +30,6 @@
     9.4  struct
     9.5  
     9.6  structure T = OuterLex;
     9.7 -structure P = OuterParse;
     9.8  
     9.9  
    9.10  (** reading instantiations **)
    9.11 @@ -215,14 +214,14 @@
    9.12    Args.internal_term >> T.Term ||
    9.13    Args.name_source >> T.Text;
    9.14  
    9.15 -val inst = Args.var -- (Args.$$$ "=" |-- Scan.ahead P.not_eof -- value)
    9.16 +val inst = Args.var -- (Args.$$$ "=" |-- Scan.ahead Parse.not_eof -- value)
    9.17    >> (fn (xi, (a, v)) => (a, (xi, v)));
    9.18  
    9.19  in
    9.20  
    9.21  val _ = Context.>> (Context.map_theory
    9.22    (Attrib.setup (Binding.name "where")
    9.23 -    (Scan.lift (P.and_list inst) >> (fn args =>
    9.24 +    (Scan.lift (Parse.and_list inst) >> (fn args =>
    9.25        Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)))
    9.26      "named instantiation of theorem"));
    9.27  
    9.28 @@ -237,7 +236,7 @@
    9.29    Args.internal_term >> T.Term ||
    9.30    Args.name_source >> T.Text;
    9.31  
    9.32 -val inst = Scan.ahead P.not_eof -- Args.maybe value;
    9.33 +val inst = Scan.ahead Parse.not_eof -- Args.maybe value;
    9.34  val concl = Args.$$$ "concl" -- Args.colon;
    9.35  
    9.36  val insts =
    9.37 @@ -387,7 +386,8 @@
    9.38  fun method inst_tac tac =
    9.39    Args.goal_spec --
    9.40    Scan.optional (Scan.lift
    9.41 -    (P.and_list1 (Args.var -- (Args.$$$ "=" |-- P.!!! Args.name_source)) --| Args.$$$ "in")) [] --
    9.42 +    (Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.name_source)) --|
    9.43 +      Args.$$$ "in")) [] --
    9.44    Attrib.thms >>
    9.45    (fn ((quant, insts), thms) => fn ctxt => METHOD (fn facts =>
    9.46      if null insts then quant (Method.insert_tac facts THEN' tac ctxt thms)
    9.47 @@ -425,5 +425,5 @@
    9.48  
    9.49  end;
    9.50  
    9.51 -structure BasicRuleInsts: BASIC_RULE_INSTS = RuleInsts;
    9.52 -open BasicRuleInsts;
    9.53 +structure Basic_Rule_Insts: BASIC_RULE_INSTS = RuleInsts;
    9.54 +open Basic_Rule_Insts;
    10.1 --- a/src/Pure/Isar/spec_parse.ML	Sat May 15 22:24:25 2010 +0200
    10.2 +++ b/src/Pure/Isar/spec_parse.ML	Sat May 15 23:16:32 2010 +0200
    10.3 @@ -35,121 +35,129 @@
    10.4  structure SpecParse: SPEC_PARSE =
    10.5  struct
    10.6  
    10.7 -structure P = OuterParse;
    10.8 -
    10.9 -
   10.10  (* theorem specifications *)
   10.11  
   10.12 -val attrib = P.position ((P.keyword_ident_or_symbolic || P.xname) -- P.!!! Args.parse) >> Args.src;
   10.13 -val attribs = P.$$$ "[" |-- P.list attrib --| P.$$$ "]";
   10.14 +val attrib =
   10.15 +  Parse.position ((Parse.keyword_ident_or_symbolic || Parse.xname) -- Parse.!!! Args.parse)
   10.16 +  >> Args.src;
   10.17 +
   10.18 +val attribs = Parse.$$$ "[" |-- Parse.list attrib --| Parse.$$$ "]";
   10.19  val opt_attribs = Scan.optional attribs [];
   10.20  
   10.21 -fun thm_name s = P.binding -- opt_attribs --| P.$$$ s;
   10.22 +fun thm_name s = Parse.binding -- opt_attribs --| Parse.$$$ s;
   10.23  
   10.24  fun opt_thm_name s =
   10.25 -  Scan.optional ((P.binding -- opt_attribs || attribs >> pair Binding.empty) --| P.$$$ s)
   10.26 +  Scan.optional ((Parse.binding -- opt_attribs || attribs >> pair Binding.empty) --| Parse.$$$ s)
   10.27      Attrib.empty_binding;
   10.28  
   10.29 -val spec = opt_thm_name ":" -- P.prop;
   10.30 -val specs = opt_thm_name ":" -- Scan.repeat1 P.prop;
   10.31 +val spec = opt_thm_name ":" -- Parse.prop;
   10.32 +val specs = opt_thm_name ":" -- Scan.repeat1 Parse.prop;
   10.33  
   10.34  val alt_specs =
   10.35 -  P.enum1 "|" (spec --| Scan.option (Scan.ahead (P.name || P.$$$ "[") -- P.!!! (P.$$$ "|")));
   10.36 +  Parse.enum1 "|"
   10.37 +    (spec --| Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|")));
   10.38  
   10.39 -val where_alt_specs = P.where_ |-- P.!!! alt_specs;
   10.40 +val where_alt_specs = Parse.where_ |-- Parse.!!! alt_specs;
   10.41  
   10.42  val xthm =
   10.43 -  P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Facts.named "") ||
   10.44 -  (P.alt_string >> Facts.Fact ||
   10.45 -    P.position P.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;
   10.46 +  Parse.$$$ "[" |-- attribs --| Parse.$$$ "]" >> pair (Facts.named "") ||
   10.47 +  (Parse.alt_string >> Facts.Fact ||
   10.48 +    Parse.position Parse.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;
   10.49  
   10.50  val xthms1 = Scan.repeat1 xthm;
   10.51  
   10.52 -val name_facts = P.and_list1 (opt_thm_name "=" -- xthms1);
   10.53 +val name_facts = Parse.and_list1 (opt_thm_name "=" -- xthms1);
   10.54  
   10.55  
   10.56  (* basic constant specifications *)
   10.57  
   10.58  val constdecl =
   10.59 -  P.binding --
   10.60 -    (P.where_ >> K (NONE, NoSyn) ||
   10.61 -      P.$$$ "::" |-- P.!!! ((P.typ >> SOME) -- P.opt_mixfix' --| P.where_) ||
   10.62 -      Scan.ahead (P.$$$ "(") |-- P.!!! (P.mixfix' --| P.where_ >> pair NONE))
   10.63 -  >> P.triple2;
   10.64 +  Parse.binding --
   10.65 +    (Parse.where_ >> K (NONE, NoSyn) ||
   10.66 +      Parse.$$$ "::" |-- Parse.!!! ((Parse.typ >> SOME) -- Parse.opt_mixfix' --| Parse.where_) ||
   10.67 +      Scan.ahead (Parse.$$$ "(") |-- Parse.!!! (Parse.mixfix' --| Parse.where_ >> pair NONE))
   10.68 +  >> Parse.triple2;
   10.69  
   10.70 -val constdef = Scan.option constdecl -- (opt_thm_name ":" -- P.prop);
   10.71 +val constdef = Scan.option constdecl -- (opt_thm_name ":" -- Parse.prop);
   10.72  
   10.73  
   10.74  (* locale and context elements *)
   10.75  
   10.76 -val locale_mixfix = P.$$$ "(" -- P.$$$ "structure" -- P.!!! (P.$$$ ")") >> K Structure || P.mixfix;
   10.77 +val locale_mixfix =
   10.78 +  Parse.$$$ "(" -- Parse.$$$ "structure" -- Parse.!!! (Parse.$$$ ")") >> K Structure ||
   10.79 +  Parse.mixfix;
   10.80  
   10.81  val locale_fixes =
   10.82 -  P.and_list1 (P.binding -- Scan.option (P.$$$ "::" |-- P.typ) -- locale_mixfix
   10.83 -    >> (single o P.triple1) ||
   10.84 -  P.params >> map Syntax.no_syn) >> flat;
   10.85 +  Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- locale_mixfix
   10.86 +    >> (single o Parse.triple1) ||
   10.87 +  Parse.params >> map Syntax.no_syn) >> flat;
   10.88  
   10.89  val locale_insts =
   10.90 -  Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) []
   10.91 -  -- Scan.optional (P.where_ |-- P.and_list1 (opt_thm_name ":" -- P.prop)) [];
   10.92 +  Scan.optional
   10.93 +    (Parse.$$$ "[" |-- Parse.!!! (Scan.repeat1 (Parse.maybe Parse.term) --| Parse.$$$ "]")) [] --
   10.94 +  Scan.optional (Parse.where_ |-- Parse.and_list1 (opt_thm_name ":" -- Parse.prop)) [];
   10.95  
   10.96  local
   10.97  
   10.98  val loc_element =
   10.99 -  P.$$$ "fixes" |-- P.!!! locale_fixes >> Element.Fixes ||
  10.100 -  P.$$$ "constrains" |-- P.!!! (P.and_list1 (P.name -- (P.$$$ "::" |-- P.typ)))
  10.101 +  Parse.$$$ "fixes" |-- Parse.!!! locale_fixes >> Element.Fixes ||
  10.102 +  Parse.$$$ "constrains" |--
  10.103 +    Parse.!!! (Parse.and_list1 (Parse.name -- (Parse.$$$ "::" |-- Parse.typ)))
  10.104      >> Element.Constrains ||
  10.105 -  P.$$$ "assumes" |-- P.!!! (P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp))
  10.106 +  Parse.$$$ "assumes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp))
  10.107      >> Element.Assumes ||
  10.108 -  P.$$$ "defines" |-- P.!!! (P.and_list1 (opt_thm_name ":" -- P.propp))
  10.109 +  Parse.$$$ "defines" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Parse.propp))
  10.110      >> Element.Defines ||
  10.111 -  P.$$$ "notes" |-- P.!!! (P.and_list1 (opt_thm_name "=" -- xthms1))
  10.112 +  Parse.$$$ "notes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name "=" -- xthms1))
  10.113      >> (curry Element.Notes "");
  10.114  
  10.115  fun plus1_unless test scan =
  10.116 -  scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
  10.117 +  scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan));
  10.118  
  10.119  fun prefix mandatory =
  10.120 -  P.name -- (P.$$$ "!" >> K true || P.$$$ "?" >> K false || Scan.succeed mandatory) --| P.$$$ ":";
  10.121 +  Parse.name --
  10.122 +    (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --|
  10.123 +    Parse.$$$ ":";
  10.124  
  10.125 -val instance = P.where_ |--
  10.126 -  P.and_list1 (P.name -- (P.$$$ "=" |-- P.term)) >> Expression.Named ||
  10.127 -  Scan.repeat1 (P.maybe P.term) >> Expression.Positional;
  10.128 +val instance = Parse.where_ |--
  10.129 +  Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named ||
  10.130 +  Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional;
  10.131  
  10.132  in
  10.133  
  10.134 -val locale_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
  10.135 -   P.$$$ "defines" || P.$$$ "notes";
  10.136 +val locale_keyword =
  10.137 +  Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" ||
  10.138 +  Parse.$$$ "defines" || Parse.$$$ "notes";
  10.139  
  10.140 -val class_expr = plus1_unless locale_keyword P.xname;
  10.141 +val class_expr = plus1_unless locale_keyword Parse.xname;
  10.142  
  10.143  fun locale_expression mandatory =
  10.144    let
  10.145 -    val expr2 = P.xname;
  10.146 +    val expr2 = Parse.xname;
  10.147      val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 --
  10.148        Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
  10.149      val expr0 = plus1_unless locale_keyword expr1;
  10.150 -  in expr0 -- Scan.optional (P.$$$ "for" |-- P.!!! locale_fixes) [] end;
  10.151 +  in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end;
  10.152  
  10.153 -val context_element = P.group "context element" loc_element;
  10.154 +val context_element = Parse.group "context element" loc_element;
  10.155  
  10.156  end;
  10.157  
  10.158  
  10.159  (* statements *)
  10.160  
  10.161 -val statement = P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp);
  10.162 +val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp);
  10.163  
  10.164  val obtain_case =
  10.165 -  P.parbinding -- (Scan.optional (P.simple_fixes --| P.where_) [] --
  10.166 -    (P.and_list1 (Scan.repeat1 P.prop) >> flat));
  10.167 +  Parse.parbinding -- (Scan.optional (Parse.simple_fixes --| Parse.where_) [] --
  10.168 +    (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat));
  10.169  
  10.170  val general_statement =
  10.171    statement >> (fn x => ([], Element.Shows x)) ||
  10.172    Scan.repeat context_element --
  10.173 -   (P.$$$ "obtains" |-- P.!!! (P.enum1 "|" obtain_case) >> Element.Obtains ||
  10.174 -    P.$$$ "shows" |-- P.!!! statement >> Element.Shows);
  10.175 +   (Parse.$$$ "obtains" |-- Parse.!!! (Parse.enum1 "|" obtain_case) >> Element.Obtains ||
  10.176 +    Parse.$$$ "shows" |-- Parse.!!! statement >> Element.Shows);
  10.177  
  10.178 -val statement_keyword = P.$$$ "obtains" || P.$$$ "shows";
  10.179 +val statement_keyword = Parse.$$$ "obtains" || Parse.$$$ "shows";
  10.180  
  10.181  end;
    11.1 --- a/src/Pure/Isar/toplevel.ML	Sat May 15 22:24:25 2010 +0200
    11.2 +++ b/src/Pure/Isar/toplevel.ML	Sat May 15 23:16:32 2010 +0200
    11.3 @@ -660,8 +660,8 @@
    11.4    let val st' = command tr st in
    11.5      if immediate orelse
    11.6        null proof_trs orelse
    11.7 -      OuterKeyword.is_schematic_goal (name_of tr) orelse
    11.8 -      exists (OuterKeyword.is_qed_global o name_of) proof_trs orelse
    11.9 +      Keyword.is_schematic_goal (name_of tr) orelse
   11.10 +      exists (Keyword.is_qed_global o name_of) proof_trs orelse
   11.11        not (can proof_of st') orelse
   11.12        Proof.is_relevant (proof_of st')
   11.13      then
    12.1 --- a/src/Pure/Isar/value_parse.ML	Sat May 15 22:24:25 2010 +0200
    12.2 +++ b/src/Pure/Isar/value_parse.ML	Sat May 15 23:16:32 2010 +0200
    12.3 @@ -19,27 +19,24 @@
    12.4  structure ValueParse: VALUE_PARSE =
    12.5  struct
    12.6  
    12.7 -structure P = OuterParse;
    12.8 -
    12.9 -
   12.10  (* syntax utilities *)
   12.11  
   12.12 -fun comma p = P.$$$ "," |-- P.!!! p;
   12.13 -fun equal p = P.$$$ "=" |-- P.!!! p;
   12.14 -fun parens p = P.$$$ "(" |-- P.!!! (p --| P.$$$ ")");
   12.15 +fun comma p = Parse.$$$ "," |-- Parse.!!! p;
   12.16 +fun equal p = Parse.$$$ "=" |-- Parse.!!! p;
   12.17 +fun parens p = Parse.$$$ "(" |-- Parse.!!! (p --| Parse.$$$ ")");
   12.18  
   12.19  
   12.20  (* tuples *)
   12.21  
   12.22  val unit = parens (Scan.succeed ());
   12.23  fun pair p1 p2 = parens (p1 -- comma p2);
   12.24 -fun triple p1 p2 p3 = parens (p1 -- comma p2 -- comma p3) >> P.triple1;
   12.25 +fun triple p1 p2 p3 = parens (p1 -- comma p2 -- comma p3) >> Parse.triple1;
   12.26  
   12.27  
   12.28  (* lists *)
   12.29  
   12.30 -fun list p = parens (P.enum "," p);
   12.31 -val properties = list (P.string -- equal P.string);
   12.32 +fun list p = parens (Parse.enum "," p);
   12.33 +val properties = list (Parse.string -- equal Parse.string);
   12.34  
   12.35  end;
   12.36  
    13.1 --- a/src/Pure/ML/ml_antiquote.ML	Sat May 15 22:24:25 2010 +0200
    13.2 +++ b/src/Pure/ML/ml_antiquote.ML	Sat May 15 23:16:32 2010 +0200
    13.3 @@ -57,12 +57,11 @@
    13.4  
    13.5  (** misc antiquotations **)
    13.6  
    13.7 -structure P = OuterParse;
    13.8 -
    13.9  val _ = inline "make_string" (Scan.succeed ml_make_string);
   13.10  
   13.11  val _ = value "binding"
   13.12 -  (Scan.lift (P.position Args.name) >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));
   13.13 +  (Scan.lift (Parse.position Args.name)
   13.14 +    >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));
   13.15  
   13.16  val _ = value "theory"
   13.17    (Scan.lift Args.name >> (fn name => "ThyInfo.get_theory " ^ ML_Syntax.print_string name)
   13.18 @@ -80,11 +79,12 @@
   13.19  val _ = inline "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term));
   13.20  
   13.21  val _ = macro "let" (Args.context --
   13.22 -  Scan.lift (P.and_list1 (P.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source)))
   13.23 +  Scan.lift
   13.24 +    (Parse.and_list1 (Parse.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source)))
   13.25      >> (fn (ctxt, args) => #2 (ProofContext.match_bind true args ctxt)));
   13.26  
   13.27  val _ = macro "note" (Args.context :|-- (fn ctxt =>
   13.28 -  P.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) =>
   13.29 +  Parse.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) =>
   13.30      ((a, map (Attrib.attribute (ProofContext.theory_of ctxt)) srcs), [(ths, [])])))
   13.31    >> (fn args => #2 (ProofContext.note_thmss "" args ctxt))));
   13.32  
   13.33 @@ -118,7 +118,7 @@
   13.34  
   13.35  (* type constructors *)
   13.36  
   13.37 -fun type_name kind check = Args.context -- Scan.lift (OuterParse.position Args.name_source)
   13.38 +fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_source)
   13.39    >> (fn (ctxt, (s, pos)) =>
   13.40      let
   13.41        val Type (c, _) = ProofContext.read_type_name_proper ctxt false s;
   13.42 @@ -137,7 +137,7 @@
   13.43  
   13.44  (* constants *)
   13.45  
   13.46 -fun const_name check = Args.context -- Scan.lift (OuterParse.position Args.name_source)
   13.47 +fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_source)
   13.48    >> (fn (ctxt, (s, pos)) =>
   13.49      let
   13.50        val Const (c, _) = ProofContext.read_const_proper ctxt false s;
   13.51 @@ -151,13 +151,13 @@
   13.52  
   13.53  
   13.54  val _ = inline "syntax_const"
   13.55 -  (Args.context -- Scan.lift (OuterParse.position Args.name) >> (fn (ctxt, (c, pos)) =>
   13.56 +  (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) =>
   13.57      if Syntax.is_const (ProofContext.syn_of ctxt) c then ML_Syntax.print_string c
   13.58      else error ("Unknown syntax const: " ^ quote c ^ Position.str_of pos)));
   13.59  
   13.60  val _ = inline "const"
   13.61    (Args.context -- Scan.lift Args.name_source -- Scan.optional
   13.62 -      (Scan.lift (Args.$$$ "(") |-- OuterParse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
   13.63 +      (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
   13.64      >> (fn ((ctxt, raw_c), Ts) =>
   13.65        let
   13.66          val Const (c, _) = ProofContext.read_const_proper ctxt true raw_c;
    14.1 --- a/src/Pure/ML/ml_context.ML	Sat May 15 22:24:25 2010 +0200
    14.2 +++ b/src/Pure/ML/ml_context.ML	Sat May 15 23:16:32 2010 +0200
    14.3 @@ -112,11 +112,10 @@
    14.4  
    14.5  local
    14.6  
    14.7 -structure P = OuterParse;
    14.8  structure T = OuterLex;
    14.9  
   14.10  val antiq =
   14.11 -  P.!!! (P.position P.xname -- Args.parse --| Scan.ahead P.eof)
   14.12 +  Parse.!!! (Parse.position Parse.xname -- Args.parse --| Scan.ahead Parse.eof)
   14.13    >> (fn ((x, pos), y) => Args.src ((x, y), pos));
   14.14  
   14.15  val begin_env = ML_Lex.tokenize "structure Isabelle =\nstruct\n";
   14.16 @@ -138,7 +137,7 @@
   14.17                NONE => error ("No context -- cannot expand ML antiquotations" ^ Position.str_of pos)
   14.18              | SOME ctxt => Context.proof_of ctxt);
   14.19  
   14.20 -          val lex = #1 (OuterKeyword.get_lexicons ());
   14.21 +          val lex = #1 (Keyword.get_lexicons ());
   14.22            fun no_decl _ = ([], []);
   14.23  
   14.24            fun expand (Antiquote.Text tok) state = (K ([], [tok]), state)
    15.1 --- a/src/Pure/ML/ml_thms.ML	Sat May 15 22:24:25 2010 +0200
    15.2 +++ b/src/Pure/ML/ml_thms.ML	Sat May 15 23:16:32 2010 +0200
    15.3 @@ -54,7 +54,7 @@
    15.4  
    15.5  val _ = ML_Context.add_antiq "lemma"
    15.6    (fn _ => Args.context -- Args.mode "open" --
    15.7 -      Scan.lift (OuterParse.and_list1 (Scan.repeat1 goal) --
    15.8 +      Scan.lift (Parse.and_list1 (Scan.repeat1 goal) --
    15.9          (by |-- Method.parse -- Scan.option Method.parse)) >>
   15.10      (fn ((ctxt, is_open), (raw_propss, methods)) => fn background =>
   15.11        let
    16.1 --- a/src/Pure/Proof/extraction.ML	Sat May 15 22:24:25 2010 +0200
    16.2 +++ b/src/Pure/Proof/extraction.ML	Sat May 15 23:16:32 2010 +0200
    16.3 @@ -750,31 +750,29 @@
    16.4  
    16.5  (**** interface ****)
    16.6  
    16.7 -structure P = OuterParse and K = OuterKeyword;
    16.8 -
    16.9 -val parse_vars = Scan.optional (P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") [];
   16.10 +val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") [];
   16.11  
   16.12  val _ =
   16.13    OuterSyntax.command "realizers"
   16.14    "specify realizers for primitive axioms / theorems, together with correctness proof"
   16.15 -  K.thy_decl
   16.16 -    (Scan.repeat1 (P.xname -- parse_vars --| P.$$$ ":" -- P.string -- P.string) >>
   16.17 +  Keyword.thy_decl
   16.18 +    (Scan.repeat1 (Parse.xname -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
   16.19       (fn xs => Toplevel.theory (fn thy => add_realizers
   16.20         (map (fn (((a, vs), s1), s2) => (PureThy.get_thm thy a, (vs, s1, s2))) xs) thy)));
   16.21  
   16.22  val _ =
   16.23    OuterSyntax.command "realizability"
   16.24 -  "add equations characterizing realizability" K.thy_decl
   16.25 -  (Scan.repeat1 P.string >> (Toplevel.theory o add_realizes_eqns));
   16.26 +  "add equations characterizing realizability" Keyword.thy_decl
   16.27 +  (Scan.repeat1 Parse.string >> (Toplevel.theory o add_realizes_eqns));
   16.28  
   16.29  val _ =
   16.30    OuterSyntax.command "extract_type"
   16.31 -  "add equations characterizing type of extracted program" K.thy_decl
   16.32 -  (Scan.repeat1 P.string >> (Toplevel.theory o add_typeof_eqns));
   16.33 +  "add equations characterizing type of extracted program" Keyword.thy_decl
   16.34 +  (Scan.repeat1 Parse.string >> (Toplevel.theory o add_typeof_eqns));
   16.35  
   16.36  val _ =
   16.37 -  OuterSyntax.command "extract" "extract terms from proofs" K.thy_decl
   16.38 -    (Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
   16.39 +  OuterSyntax.command "extract" "extract terms from proofs" Keyword.thy_decl
   16.40 +    (Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
   16.41        extract (map (apfst (PureThy.get_thm thy)) xs) thy)));
   16.42  
   16.43  val etype_of = etype_of o add_syntax;
    17.1 --- a/src/Pure/ProofGeneral/pgip_parser.ML	Sat May 15 22:24:25 2010 +0200
    17.2 +++ b/src/Pure/ProofGeneral/pgip_parser.ML	Sat May 15 23:16:32 2010 +0200
    17.3 @@ -12,7 +12,6 @@
    17.4  structure PgipParser: PGIP_PARSER =
    17.5  struct
    17.6  
    17.7 -structure K = OuterKeyword;
    17.8  structure D = PgipMarkup;
    17.9  structure I = PgipIsabelle;
   17.10  
   17.11 @@ -51,42 +50,42 @@
   17.12  fun closegoal text = [D.Closegoal {text = text}, D.Closeblock {}];
   17.13  
   17.14  
   17.15 -fun command k f = Symtab.update_new (OuterKeyword.kind_of k, f);
   17.16 +fun command k f = Symtab.update_new (Keyword.kind_of k, f);
   17.17  
   17.18  val command_keywords = Symtab.empty
   17.19 -  |> command K.control          badcmd
   17.20 -  |> command K.diag             (fn text => [D.Spuriouscmd {text = text}])
   17.21 -  |> command K.thy_begin        thy_begin
   17.22 -  |> command K.thy_switch       badcmd
   17.23 -  |> command K.thy_end          (fn text => [D.Closeblock {}, D.Closetheory {text = text}])
   17.24 -  |> command K.thy_heading      thy_heading
   17.25 -  |> command K.thy_decl         thy_decl
   17.26 -  |> command K.thy_script       thy_decl
   17.27 -  |> command K.thy_goal         goal
   17.28 -  |> command K.thy_schematic_goal goal
   17.29 -  |> command K.qed              closegoal
   17.30 -  |> command K.qed_block        closegoal
   17.31 -  |> command K.qed_global       (fn text => [D.Giveupgoal {text = text}])
   17.32 -  |> command K.prf_heading      (fn text => [D.Doccomment {text = text}])
   17.33 -  |> command K.prf_goal         goal
   17.34 -  |> command K.prf_block        prf_block
   17.35 -  |> command K.prf_open         prf_open
   17.36 -  |> command K.prf_close        (fn text => [D.Proofstep {text = text}, D.Closeblock {}])
   17.37 -  |> command K.prf_chain        proofstep
   17.38 -  |> command K.prf_decl         proofstep
   17.39 -  |> command K.prf_asm          proofstep
   17.40 -  |> command K.prf_asm_goal     goal
   17.41 -  |> command K.prf_script       proofstep;
   17.42 +  |> command Keyword.control          badcmd
   17.43 +  |> command Keyword.diag             (fn text => [D.Spuriouscmd {text = text}])
   17.44 +  |> command Keyword.thy_begin        thy_begin
   17.45 +  |> command Keyword.thy_switch       badcmd
   17.46 +  |> command Keyword.thy_end          (fn text => [D.Closeblock {}, D.Closetheory {text = text}])
   17.47 +  |> command Keyword.thy_heading      thy_heading
   17.48 +  |> command Keyword.thy_decl         thy_decl
   17.49 +  |> command Keyword.thy_script       thy_decl
   17.50 +  |> command Keyword.thy_goal         goal
   17.51 +  |> command Keyword.thy_schematic_goal goal
   17.52 +  |> command Keyword.qed              closegoal
   17.53 +  |> command Keyword.qed_block        closegoal
   17.54 +  |> command Keyword.qed_global       (fn text => [D.Giveupgoal {text = text}])
   17.55 +  |> command Keyword.prf_heading      (fn text => [D.Doccomment {text = text}])
   17.56 +  |> command Keyword.prf_goal         goal
   17.57 +  |> command Keyword.prf_block        prf_block
   17.58 +  |> command Keyword.prf_open         prf_open
   17.59 +  |> command Keyword.prf_close        (fn text => [D.Proofstep {text = text}, D.Closeblock {}])
   17.60 +  |> command Keyword.prf_chain        proofstep
   17.61 +  |> command Keyword.prf_decl         proofstep
   17.62 +  |> command Keyword.prf_asm          proofstep
   17.63 +  |> command Keyword.prf_asm_goal     goal
   17.64 +  |> command Keyword.prf_script       proofstep;
   17.65  
   17.66 -val _ = subset (op =) (OuterKeyword.kinds, Symtab.keys command_keywords)
   17.67 +val _ = subset (op =) (Keyword.kinds, Symtab.keys command_keywords)
   17.68    orelse sys_error "Incomplete coverage of command keywords";
   17.69  
   17.70  fun parse_command "sorry" text = [D.Postponegoal {text = text}, D.Closeblock {}]
   17.71    | parse_command name text =
   17.72 -      (case OuterKeyword.command_keyword name of
   17.73 +      (case Keyword.command_keyword name of
   17.74          NONE => [D.Unparseable {text = text}]
   17.75        | SOME k =>
   17.76 -          (case Symtab.lookup command_keywords (OuterKeyword.kind_of k) of
   17.77 +          (case Symtab.lookup command_keywords (Keyword.kind_of k) of
   17.78              NONE => [D.Unparseable {text = text}]
   17.79            | SOME f => f text));
   17.80  
   17.81 @@ -104,6 +103,6 @@
   17.82  
   17.83  
   17.84  fun pgip_parser pos str =
   17.85 -  maps parse_span (ThySyntax.parse_spans (OuterKeyword.get_lexicons ()) pos str);
   17.86 +  maps parse_span (ThySyntax.parse_spans (Keyword.get_lexicons ()) pos str);
   17.87  
   17.88  end;
    18.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat May 15 22:24:25 2010 +0200
    18.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat May 15 23:16:32 2010 +0200
    18.3 @@ -188,48 +188,44 @@
    18.4  
    18.5  (* additional outer syntax for Isar *)
    18.6  
    18.7 -local structure P = OuterParse and K = OuterKeyword in
    18.8 -
    18.9  fun prP () =
   18.10 -  OuterSyntax.improper_command "ProofGeneral.pr" "print state (internal)" K.diag
   18.11 +  OuterSyntax.improper_command "ProofGeneral.pr" "print state (internal)" Keyword.diag
   18.12      (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
   18.13        if Toplevel.is_toplevel state orelse Toplevel.is_theory state then tell_clear_goals ()
   18.14        else (Toplevel.quiet := false; Toplevel.print_state true state))));
   18.15  
   18.16  fun undoP () = (*undo without output -- historical*)
   18.17 -  OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
   18.18 +  OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" Keyword.control
   18.19      (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1)));
   18.20  
   18.21  fun restartP () =
   18.22 -  OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
   18.23 -    (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
   18.24 +  OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" Keyword.control
   18.25 +    (Parse.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
   18.26  
   18.27  fun kill_proofP () =
   18.28 -  OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
   18.29 +  OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" Keyword.control
   18.30      (Scan.succeed (Toplevel.no_timing o
   18.31        Toplevel.imperative (fn () => (Isar.kill_proof (); tell_clear_goals ()))));
   18.32  
   18.33  fun inform_file_processedP () =
   18.34 -  OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
   18.35 -    (P.name >> (fn file =>
   18.36 +  OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" Keyword.control
   18.37 +    (Parse.name >> (fn file =>
   18.38        Toplevel.no_timing o Toplevel.imperative (fn () => inform_file_processed file)));
   18.39  
   18.40  fun inform_file_retractedP () =
   18.41 -  OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
   18.42 -    (P.name >> (Toplevel.no_timing oo
   18.43 +  OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" Keyword.control
   18.44 +    (Parse.name >> (Toplevel.no_timing oo
   18.45        (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
   18.46  
   18.47  fun process_pgipP () =
   18.48 -  OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
   18.49 -    (P.text >> (Toplevel.no_timing oo
   18.50 +  OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" Keyword.control
   18.51 +    (Parse.text >> (Toplevel.no_timing oo
   18.52        (fn txt => Toplevel.imperative (fn () => ProofGeneralPgip.process_pgip txt))));
   18.53  
   18.54  fun init_outer_syntax () = List.app (fn f => f ())
   18.55    [prP, undoP, restartP, kill_proofP, inform_file_processedP,
   18.56      inform_file_retractedP, process_pgipP];
   18.57  
   18.58 -end;
   18.59 -
   18.60  
   18.61  (* init *)
   18.62  
    19.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat May 15 22:24:25 2010 +0200
    19.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat May 15 23:16:32 2010 +0200
    19.3 @@ -312,8 +312,8 @@
    19.4  (** lexicalstructure element with keywords (PGIP version of elisp keywords file) **)
    19.5  
    19.6  fun lexicalstructure_keywords () =
    19.7 -    let val keywords = OuterKeyword.dest_keywords ()
    19.8 -        val commands = OuterKeyword.dest_commands ()
    19.9 +    let val keywords = Keyword.dest_keywords ()
   19.10 +        val commands = Keyword.dest_commands ()
   19.11          fun keyword_elt kind keyword =
   19.12              XML.Elem("keyword", [("word", keyword), ("category", kind)], [])
   19.13          in
   19.14 @@ -1013,8 +1013,8 @@
   19.15  (* Extra command for embedding prover-control inside document (obscure/debug usage). *)
   19.16  
   19.17  fun init_outer_syntax () =
   19.18 -  OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" OuterKeyword.control
   19.19 -    (OuterParse.text >> (Toplevel.no_timing oo
   19.20 +  OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" Keyword.control
   19.21 +    (Parse.text >> (Toplevel.no_timing oo
   19.22        (fn txt => Toplevel.imperative (fn () => process_pgip_plain txt))));
   19.23  
   19.24  
    20.1 --- a/src/Pure/System/isabelle_process.ML	Sat May 15 22:24:25 2010 +0200
    20.2 +++ b/src/Pure/System/isabelle_process.ML	Sat May 15 23:16:32 2010 +0200
    20.3 @@ -89,9 +89,9 @@
    20.4  
    20.5  fun init out =
    20.6   (Unsynchronized.change print_mode
    20.7 -    (fold (update op =) [isabelle_processN, OuterKeyword.keyword_status_reportN, Pretty.symbolicN]);
    20.8 +    (fold (update op =) [isabelle_processN, Keyword.keyword_status_reportN, Pretty.symbolicN]);
    20.9    setup_channels out |> init_message;
   20.10 -  OuterKeyword.report ();
   20.11 +  Keyword.report ();
   20.12    Output.status (Markup.markup Markup.ready "");
   20.13    Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
   20.14  
    21.1 --- a/src/Pure/System/isar.ML	Sat May 15 22:24:25 2010 +0200
    21.2 +++ b/src/Pure/System/isar.ML	Sat May 15 23:16:32 2010 +0200
    21.3 @@ -80,14 +80,14 @@
    21.4  fun linear_undo n = edit_history n (K (find_and_undo (K true)));
    21.5  
    21.6  fun undo n = edit_history n (fn st => fn hist =>
    21.7 -  find_and_undo (if Toplevel.is_proof st then K true else OuterKeyword.is_theory) hist);
    21.8 +  find_and_undo (if Toplevel.is_proof st then K true else Keyword.is_theory) hist);
    21.9  
   21.10  fun kill () = edit_history 1 (fn st => fn hist =>
   21.11    find_and_undo
   21.12 -    (if Toplevel.is_proof st then OuterKeyword.is_theory else OuterKeyword.is_theory_begin) hist);
   21.13 +    (if Toplevel.is_proof st then Keyword.is_theory else Keyword.is_theory_begin) hist);
   21.14  
   21.15  fun kill_proof () = edit_history 1 (fn st => fn hist =>
   21.16 -  if Toplevel.is_proof st then find_and_undo OuterKeyword.is_theory hist
   21.17 +  if Toplevel.is_proof st then find_and_undo Keyword.is_theory hist
   21.18    else raise Toplevel.UNDEF);
   21.19  
   21.20  end;
   21.21 @@ -102,9 +102,9 @@
   21.22    | SOME (st', NONE) =>
   21.23        let
   21.24          val name = Toplevel.name_of tr;
   21.25 -        val _ = if OuterKeyword.is_theory_begin name then init () else ();
   21.26 +        val _ = if Keyword.is_theory_begin name then init () else ();
   21.27          val _ =
   21.28 -          if OuterKeyword.is_regular name
   21.29 +          if Keyword.is_regular name
   21.30            then edit_history 1 (fn st => fn hist => (st', (st, tr) :: hist)) else ();
   21.31        in true end);
   21.32  
   21.33 @@ -157,7 +157,6 @@
   21.34  
   21.35  local
   21.36  
   21.37 -structure P = OuterParse and K = OuterKeyword;
   21.38  val op >> = Scan.>>;
   21.39  
   21.40  in
   21.41 @@ -165,33 +164,35 @@
   21.42  (* global history *)
   21.43  
   21.44  val _ =
   21.45 -  OuterSyntax.improper_command "init_toplevel" "init toplevel point-of-interest" K.control
   21.46 +  OuterSyntax.improper_command "init_toplevel" "init toplevel point-of-interest" Keyword.control
   21.47      (Scan.succeed (Toplevel.no_timing o Toplevel.imperative init));
   21.48  
   21.49  val _ =
   21.50 -  OuterSyntax.improper_command "linear_undo" "undo commands" K.control
   21.51 -    (Scan.optional P.nat 1 >>
   21.52 +  OuterSyntax.improper_command "linear_undo" "undo commands" Keyword.control
   21.53 +    (Scan.optional Parse.nat 1 >>
   21.54        (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => linear_undo n)));
   21.55  
   21.56  val _ =
   21.57 -  OuterSyntax.improper_command "undo" "undo commands (skipping closed proofs)" K.control
   21.58 -    (Scan.optional P.nat 1 >>
   21.59 +  OuterSyntax.improper_command "undo" "undo commands (skipping closed proofs)" Keyword.control
   21.60 +    (Scan.optional Parse.nat 1 >>
   21.61        (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => undo n)));
   21.62  
   21.63  val _ =
   21.64 -  OuterSyntax.improper_command "undos_proof" "undo commands (skipping closed proofs)" K.control
   21.65 -    (Scan.optional P.nat 1 >> (fn n => Toplevel.no_timing o
   21.66 +  OuterSyntax.improper_command "undos_proof" "undo commands (skipping closed proofs)"
   21.67 +    Keyword.control
   21.68 +    (Scan.optional Parse.nat 1 >> (fn n => Toplevel.no_timing o
   21.69        Toplevel.keep (fn state =>
   21.70          if Toplevel.is_proof state then (undo n; print ()) else raise Toplevel.UNDEF)));
   21.71  
   21.72  val _ =
   21.73 -  OuterSyntax.improper_command "cannot_undo" "partial undo -- Proof General legacy" K.control
   21.74 -    (P.name >>
   21.75 +  OuterSyntax.improper_command "cannot_undo" "partial undo -- Proof General legacy"
   21.76 +    Keyword.control
   21.77 +    (Parse.name >>
   21.78        (fn "end" => Toplevel.no_timing o Toplevel.imperative (fn () => undo 1)
   21.79          | txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt))));
   21.80  
   21.81  val _ =
   21.82 -  OuterSyntax.improper_command "kill" "kill partial proof or theory development" K.control
   21.83 +  OuterSyntax.improper_command "kill" "kill partial proof or theory development" Keyword.control
   21.84      (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
   21.85  
   21.86  end;
    22.1 --- a/src/Pure/System/session.ML	Sat May 15 22:24:25 2010 +0200
    22.2 +++ b/src/Pure/System/session.ML	Sat May 15 23:16:32 2010 +0200
    22.3 @@ -48,7 +48,7 @@
    22.4      (if Distribution.changelog <> "" then "\nSee also " ^ Distribution.changelog else "");
    22.5  
    22.6  val _ =
    22.7 -  OuterSyntax.improper_command "welcome" "print welcome message" OuterKeyword.diag
    22.8 +  OuterSyntax.improper_command "welcome" "print welcome message" Keyword.diag
    22.9      (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (writeln o welcome)));
   22.10  
   22.11  
    23.1 --- a/src/Pure/Thy/term_style.ML	Sat May 15 22:24:25 2010 +0200
    23.2 +++ b/src/Pure/Thy/term_style.ML	Sat May 15 23:16:32 2010 +0200
    23.3 @@ -43,7 +43,7 @@
    23.4  
    23.5  (* style parsing *)
    23.6  
    23.7 -fun parse_single ctxt = OuterParse.position (OuterParse.xname -- Args.parse)
    23.8 +fun parse_single ctxt = Parse.position (Parse.xname -- Args.parse)
    23.9    >> (fn x as ((name, _), _) => fst (Args.context_syntax "style"
   23.10         (Scan.lift (the_style (ProofContext.theory_of ctxt) name))
   23.11           (Args.src x) ctxt |>> (fn f => f ctxt)));
    24.1 --- a/src/Pure/Thy/thy_header.ML	Sat May 15 22:24:25 2010 +0200
    24.2 +++ b/src/Pure/Thy/thy_header.ML	Sat May 15 23:16:32 2010 +0200
    24.3 @@ -15,7 +15,6 @@
    24.4  struct
    24.5  
    24.6  structure T = OuterLex;
    24.7 -structure P = OuterParse;
    24.8  
    24.9  
   24.10  (* keywords *)
   24.11 @@ -32,23 +31,28 @@
   24.12  
   24.13  (* header args *)
   24.14  
   24.15 -val file_name = P.group "file name" P.name;
   24.16 -val theory_name = P.group "theory name" P.name;
   24.17 +val file_name = Parse.group "file name" Parse.name;
   24.18 +val theory_name = Parse.group "theory name" Parse.name;
   24.19  
   24.20 -val file = P.$$$ "(" |-- P.!!! (file_name --| P.$$$ ")") >> rpair false || file_name >> rpair true;
   24.21 -val uses = Scan.optional (P.$$$ usesN |-- P.!!! (Scan.repeat1 file)) [];
   24.22 +val file =
   24.23 +  Parse.$$$ "(" |-- Parse.!!! (file_name --| Parse.$$$ ")") >> rpair false ||
   24.24 +  file_name >> rpair true;
   24.25 +
   24.26 +val uses = Scan.optional (Parse.$$$ usesN |-- Parse.!!! (Scan.repeat1 file)) [];
   24.27  
   24.28  val args =
   24.29 -  theory_name -- (P.$$$ importsN |-- P.!!! (Scan.repeat1 theory_name -- uses --| P.$$$ beginN))
   24.30 -  >> P.triple2;
   24.31 +  theory_name -- (Parse.$$$ importsN |--
   24.32 +    Parse.!!! (Scan.repeat1 theory_name -- uses --| Parse.$$$ beginN))
   24.33 +  >> Parse.triple2;
   24.34  
   24.35  
   24.36  (* read header *)
   24.37  
   24.38  val header =
   24.39 -  (P.$$$ headerN -- P.tags) |-- (P.!!! (P.doc_source -- Scan.repeat P.semicolon --
   24.40 -    (P.$$$ theoryN -- P.tags) |-- args)) ||
   24.41 -  (P.$$$ theoryN -- P.tags) |-- P.!!! args;
   24.42 +  (Parse.$$$ headerN -- Parse.tags) |--
   24.43 +    (Parse.!!! (Parse.doc_source -- Scan.repeat Parse.semicolon --
   24.44 +      (Parse.$$$ theoryN -- Parse.tags) |-- args)) ||
   24.45 +  (Parse.$$$ theoryN -- Parse.tags) |-- Parse.!!! args;
   24.46  
   24.47  fun read pos src =
   24.48    let val res =
   24.49 @@ -56,7 +60,7 @@
   24.50      |> Symbol.source {do_recover = false}
   24.51      |> T.source {do_recover = NONE} (fn () => (header_lexicon, Scan.empty_lexicon)) pos
   24.52      |> T.source_proper
   24.53 -    |> Source.source T.stopper (Scan.single (Scan.error (P.!!! header))) NONE
   24.54 +    |> Source.source T.stopper (Scan.single (Scan.error (Parse.!!! header))) NONE
   24.55      |> Source.get_single;
   24.56    in
   24.57      (case res of SOME (x, _) => x
    25.1 --- a/src/Pure/Thy/thy_output.ML	Sat May 15 22:24:25 2010 +0200
    25.2 +++ b/src/Pure/Thy/thy_output.ML	Sat May 15 23:16:32 2010 +0200
    25.3 @@ -37,7 +37,6 @@
    25.4  struct
    25.5  
    25.6  structure T = OuterLex;
    25.7 -structure P = OuterParse;
    25.8  
    25.9  
   25.10  (** global options **)
   25.11 @@ -132,12 +131,16 @@
   25.12  
   25.13  local
   25.14  
   25.15 -val property = P.xname -- Scan.optional (P.$$$ "=" |-- P.!!! P.xname) "";
   25.16 -val properties = Scan.optional (P.$$$ "[" |-- P.!!! (P.enum "," property --| P.$$$ "]")) [];
   25.17 +val property =
   25.18 +  Parse.xname -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.xname) "";
   25.19 +
   25.20 +val properties =
   25.21 +  Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.enum "," property --| Parse.$$$ "]")) [];
   25.22  
   25.23  in
   25.24  
   25.25 -val antiq = P.!!! (P.position P.xname -- properties -- Args.parse --| Scan.ahead P.eof)
   25.26 +val antiq =
   25.27 +  Parse.!!! (Parse.position Parse.xname -- properties -- Args.parse --| Scan.ahead Parse.eof)
   25.28    >> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos)));
   25.29  
   25.30  end;
   25.31 @@ -249,7 +252,7 @@
   25.32      val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span;
   25.33  
   25.34      val (tag, tags) = tag_stack;
   25.35 -    val tag' = try hd (fold OuterKeyword.update_tags cmd_tags (the_list tag));
   25.36 +    val tag' = try hd (fold Keyword.update_tags cmd_tags (the_list tag));
   25.37  
   25.38      val active_tag' =
   25.39        if is_some tag' then tag'
   25.40 @@ -316,11 +319,11 @@
   25.41      (if d = 0 then Scan.fail_with (K "Bad nesting of meta-comments") else opt_newline)
   25.42      >> pair (d - 1));
   25.43  
   25.44 -val tag = (improper -- P.$$$ "%" -- improper) |-- P.!!! (P.tag_name --| blank_end);
   25.45 +val tag = (improper -- Parse.$$$ "%" -- improper) |-- Parse.!!! (Parse.tag_name --| blank_end);
   25.46  
   25.47  val locale =
   25.48 -  Scan.option ((P.$$$ "(" -- improper -- P.$$$ "in") |--
   25.49 -    P.!!! (improper |-- P.xname --| (improper -- P.$$$ ")")));
   25.50 +  Scan.option ((Parse.$$$ "(" -- improper -- Parse.$$$ "in") |--
   25.51 +    Parse.!!! (improper |-- Parse.xname --| (improper -- Parse.$$$ ")")));
   25.52  
   25.53  in
   25.54  
   25.55 @@ -332,26 +335,27 @@
   25.56        >> (fn d => (NONE, (NoToken, ("", d))));
   25.57  
   25.58      fun markup mark mk flag = Scan.peek (fn d =>
   25.59 -      improper |-- P.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.content_of)) --
   25.60 +      improper |--
   25.61 +        Parse.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.content_of)) --
   25.62        Scan.repeat tag --
   25.63 -      P.!!!! ((improper -- locale -- improper) |-- P.doc_source --| improper_end)
   25.64 +      Parse.!!!! ((improper -- locale -- improper) |-- Parse.doc_source --| improper_end)
   25.65        >> (fn (((tok, pos), tags), txt) =>
   25.66          let val name = T.content_of tok
   25.67          in (SOME (name, pos, tags), (mk (name, txt), (flag, d))) end));
   25.68  
   25.69      val command = Scan.peek (fn d =>
   25.70 -      P.position (Scan.one (T.is_kind T.Command)) --
   25.71 +      Parse.position (Scan.one (T.is_kind T.Command)) --
   25.72        Scan.repeat tag
   25.73        >> (fn ((tok, pos), tags) =>
   25.74          let val name = T.content_of tok
   25.75          in (SOME (name, pos, tags), (BasicToken tok, (Latex.markup_false, d))) end));
   25.76  
   25.77      val cmt = Scan.peek (fn d =>
   25.78 -      P.$$$ "--" |-- P.!!!! (improper |-- P.doc_source)
   25.79 +      Parse.$$$ "--" |-- Parse.!!!! (improper |-- Parse.doc_source)
   25.80        >> (fn txt => (NONE, (MarkupToken ("cmt", txt), ("", d)))));
   25.81  
   25.82      val other = Scan.peek (fn d =>
   25.83 -       P.not_eof >> (fn tok => (NONE, (BasicToken tok, ("", d)))));
   25.84 +       Parse.not_eof >> (fn tok => (NONE, (BasicToken tok, ("", d)))));
   25.85  
   25.86      val token =
   25.87        ignored ||
   25.88 @@ -565,7 +569,7 @@
   25.89  
   25.90  (* embedded lemma *)
   25.91  
   25.92 -val _ = OuterKeyword.keyword "by";
   25.93 +val _ = Keyword.keyword "by";
   25.94  
   25.95  val _ = antiquotation "lemma"
   25.96    (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse))
    26.1 --- a/src/Pure/Thy/thy_syntax.ML	Sat May 15 22:24:25 2010 +0200
    26.2 +++ b/src/Pure/Thy/thy_syntax.ML	Sat May 15 23:16:32 2010 +0200
    26.3 @@ -29,9 +29,7 @@
    26.4  structure ThySyntax: THY_SYNTAX =
    26.5  struct
    26.6  
    26.7 -structure K = OuterKeyword;
    26.8  structure T = OuterLex;
    26.9 -structure P = OuterParse;
   26.10  
   26.11  
   26.12  (** tokens **)
   26.13 @@ -111,10 +109,11 @@
   26.14  
   26.15  val is_whitespace = T.is_kind T.Space orf T.is_kind T.Comment;
   26.16  
   26.17 -val body = Scan.unless (Scan.many is_whitespace -- Scan.ahead (P.command || P.eof)) P.not_eof;
   26.18 +val body =
   26.19 +  Scan.unless (Scan.many is_whitespace -- Scan.ahead (Parse.command || Parse.eof)) Parse.not_eof;
   26.20  
   26.21  val span =
   26.22 -  Scan.ahead P.command -- P.not_eof -- Scan.repeat body
   26.23 +  Scan.ahead Parse.command -- Parse.not_eof -- Scan.repeat body
   26.24      >> (fn ((name, c), bs) => Span (Command name, c :: bs)) ||
   26.25    Scan.many1 is_whitespace >> (fn toks => Span (Ignored, toks)) ||
   26.26    Scan.repeat1 body >> (fn toks => Span (Malformed, toks));
   26.27 @@ -175,13 +174,13 @@
   26.28  val proof = Scan.pass 1 (Scan.repeat (Scan.depend (fn d =>
   26.29    if d <= 0 then Scan.fail
   26.30    else
   26.31 -    command_with K.is_qed_global >> pair ~1 ||
   26.32 -    command_with K.is_proof_goal >> pair (d + 1) ||
   26.33 -    (if d = 0 then Scan.fail else command_with K.is_qed >> pair (d - 1)) ||
   26.34 -    Scan.unless (command_with K.is_theory) (Scan.one not_eof) >> pair d)) -- Scan.state);
   26.35 +    command_with Keyword.is_qed_global >> pair ~1 ||
   26.36 +    command_with Keyword.is_proof_goal >> pair (d + 1) ||
   26.37 +    (if d = 0 then Scan.fail else command_with Keyword.is_qed >> pair (d - 1)) ||
   26.38 +    Scan.unless (command_with Keyword.is_theory) (Scan.one not_eof) >> pair d)) -- Scan.state);
   26.39  
   26.40  val unit =
   26.41 -  command_with K.is_theory_goal -- proof >> (fn (a, (bs, d)) => (a, bs, d >= 0)) ||
   26.42 +  command_with Keyword.is_theory_goal -- proof >> (fn (a, (bs, d)) => (a, bs, d >= 0)) ||
   26.43    Scan.one not_eof >> (fn a => (a, [], true));
   26.44  
   26.45  in
    27.1 --- a/src/Pure/Tools/find_consts.ML	Sat May 15 22:24:25 2010 +0200
    27.2 +++ b/src/Pure/Tools/find_consts.ML	Sat May 15 23:16:32 2010 +0200
    27.3 @@ -148,23 +148,15 @@
    27.4    Toplevel.unknown_theory o Toplevel.keep (fn state =>
    27.5      find_consts (Proof.context_of (Toplevel.enter_proof_body state)) spec);
    27.6  
    27.7 -local
    27.8 -
    27.9 -structure P = OuterParse and K = OuterKeyword;
   27.10 -
   27.11  val criterion =
   27.12 -  P.reserved "strict" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Strict ||
   27.13 -  P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Name ||
   27.14 -  P.xname >> Loose;
   27.15 -
   27.16 -in
   27.17 +  Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Strict ||
   27.18 +  Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
   27.19 +  Parse.xname >> Loose;
   27.20  
   27.21  val _ =
   27.22 -  OuterSyntax.improper_command "find_consts" "search constants by type pattern" K.diag
   27.23 -    (Scan.repeat ((Scan.option P.minus >> is_none) -- criterion)
   27.24 +  OuterSyntax.improper_command "find_consts" "search constants by type pattern" Keyword.diag
   27.25 +    (Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion)
   27.26        >> (Toplevel.no_timing oo find_consts_cmd));
   27.27  
   27.28  end;
   27.29  
   27.30 -end;
   27.31 -
    28.1 --- a/src/Pure/Tools/find_theorems.ML	Sat May 15 22:24:25 2010 +0200
    28.2 +++ b/src/Pure/Tools/find_theorems.ML	Sat May 15 23:16:32 2010 +0200
    28.3 @@ -465,28 +465,27 @@
    28.4  
    28.5  local
    28.6  
    28.7 -structure P = OuterParse and K = OuterKeyword;
    28.8 -
    28.9  val criterion =
   28.10 -  P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Name ||
   28.11 -  P.reserved "intro" >> K Intro ||
   28.12 -  P.reserved "introiff" >> K IntroIff ||
   28.13 -  P.reserved "elim" >> K Elim ||
   28.14 -  P.reserved "dest" >> K Dest ||
   28.15 -  P.reserved "solves" >> K Solves ||
   28.16 -  P.reserved "simp" |-- P.!!! (P.$$$ ":" |-- P.term) >> Simp ||
   28.17 -  P.term >> Pattern;
   28.18 +  Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
   28.19 +  Parse.reserved "intro" >> K Intro ||
   28.20 +  Parse.reserved "introiff" >> K IntroIff ||
   28.21 +  Parse.reserved "elim" >> K Elim ||
   28.22 +  Parse.reserved "dest" >> K Dest ||
   28.23 +  Parse.reserved "solves" >> K Solves ||
   28.24 +  Parse.reserved "simp" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.term) >> Simp ||
   28.25 +  Parse.term >> Pattern;
   28.26  
   28.27  val options =
   28.28    Scan.optional
   28.29 -    (P.$$$ "(" |--
   28.30 -      P.!!! (Scan.option P.nat -- Scan.optional (P.reserved "with_dups" >> K false) true
   28.31 -        --| P.$$$ ")")) (NONE, true);
   28.32 +    (Parse.$$$ "(" |--
   28.33 +      Parse.!!! (Scan.option Parse.nat -- Scan.optional (Parse.reserved "with_dups" >> K false) true
   28.34 +        --| Parse.$$$ ")")) (NONE, true);
   28.35  in
   28.36  
   28.37  val _ =
   28.38 -  OuterSyntax.improper_command "find_theorems" "print theorems meeting specified criteria" K.diag
   28.39 -    (options -- Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
   28.40 +  OuterSyntax.improper_command "find_theorems" "print theorems meeting specified criteria"
   28.41 +    Keyword.diag
   28.42 +    (options -- Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion))
   28.43        >> (Toplevel.no_timing oo find_theorems_cmd));
   28.44  
   28.45  end;
    29.1 --- a/src/Pure/codegen.ML	Sat May 15 22:24:25 2010 +0200
    29.2 +++ b/src/Pure/codegen.ML	Sat May 15 23:16:32 2010 +0200
    29.3 @@ -959,44 +959,42 @@
    29.4     | _ => error ("Malformed annotation: " ^ quote s));
    29.5  
    29.6  
    29.7 -structure P = OuterParse and K = OuterKeyword;
    29.8 -
    29.9 -val _ = List.app OuterKeyword.keyword ["attach", "file", "contains"];
   29.10 +val _ = List.app Keyword.keyword ["attach", "file", "contains"];
   29.11  
   29.12  fun strip_whitespace s = implode (fst (take_suffix (fn c => c = "\n" orelse c = " ")
   29.13    (snd (take_prefix (fn c => c = "\n" orelse c = " ") (explode s))))) ^ "\n";
   29.14  
   29.15 -val parse_attach = Scan.repeat (P.$$$ "attach" |--
   29.16 -  Scan.optional (P.$$$ "(" |-- P.xname --| P.$$$ ")") "" --
   29.17 -    (P.verbatim >> strip_whitespace));
   29.18 +val parse_attach = Scan.repeat (Parse.$$$ "attach" |--
   29.19 +  Scan.optional (Parse.$$$ "(" |-- Parse.xname --| Parse.$$$ ")") "" --
   29.20 +    (Parse.verbatim >> strip_whitespace));
   29.21  
   29.22  val _ =
   29.23    OuterSyntax.command "types_code"
   29.24 -  "associate types with target language types" K.thy_decl
   29.25 -    (Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
   29.26 +  "associate types with target language types" Keyword.thy_decl
   29.27 +    (Scan.repeat1 (Parse.xname --| Parse.$$$ "(" -- Parse.string --| Parse.$$$ ")" -- parse_attach) >>
   29.28       (fn xs => Toplevel.theory (fn thy => fold (assoc_type o
   29.29         (fn ((name, mfx), aux) => (name, (parse_mixfix
   29.30           (Syntax.read_typ_global thy) mfx, aux)))) xs thy)));
   29.31  
   29.32  val _ =
   29.33    OuterSyntax.command "consts_code"
   29.34 -  "associate constants with target language code" K.thy_decl
   29.35 +  "associate constants with target language code" Keyword.thy_decl
   29.36      (Scan.repeat1
   29.37 -       (P.term --|
   29.38 -        P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
   29.39 +       (Parse.term --|
   29.40 +        Parse.$$$ "(" -- Parse.string --| Parse.$$$ ")" -- parse_attach) >>
   29.41       (fn xs => Toplevel.theory (fn thy => fold (assoc_const o
   29.42         (fn ((const, mfx), aux) =>
   29.43           (const, (parse_mixfix (Syntax.read_term_global thy) mfx, aux)))) xs thy)));
   29.44  
   29.45  fun parse_code lib =
   29.46 -  Scan.optional (P.$$$ "(" |-- P.enum "," P.xname --| P.$$$ ")") (!mode) --
   29.47 -  (if lib then Scan.optional P.name "" else P.name) --
   29.48 -  Scan.option (P.$$$ "file" |-- P.name) --
   29.49 +  Scan.optional (Parse.$$$ "(" |-- Parse.enum "," Parse.xname --| Parse.$$$ ")") (!mode) --
   29.50 +  (if lib then Scan.optional Parse.name "" else Parse.name) --
   29.51 +  Scan.option (Parse.$$$ "file" |-- Parse.name) --
   29.52    (if lib then Scan.succeed []
   29.53 -   else Scan.optional (P.$$$ "imports" |-- Scan.repeat1 P.name) []) --|
   29.54 -  P.$$$ "contains" --
   29.55 -  (   Scan.repeat1 (P.name --| P.$$$ "=" -- P.term)
   29.56 -   || Scan.repeat1 (P.term >> pair "")) >>
   29.57 +   else Scan.optional (Parse.$$$ "imports" |-- Scan.repeat1 Parse.name) []) --|
   29.58 +  Parse.$$$ "contains" --
   29.59 +  (   Scan.repeat1 (Parse.name --| Parse.$$$ "=" -- Parse.term)
   29.60 +   || Scan.repeat1 (Parse.term >> pair "")) >>
   29.61    (fn ((((mode', module), opt_fname), modules), xs) => Toplevel.theory (fn thy =>
   29.62      let
   29.63        val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode');
   29.64 @@ -1021,12 +1019,12 @@
   29.65  
   29.66  val _ =
   29.67    OuterSyntax.command "code_library"
   29.68 -    "generates code for terms (one structure for each theory)" K.thy_decl
   29.69 +    "generates code for terms (one structure for each theory)" Keyword.thy_decl
   29.70      (parse_code true);
   29.71  
   29.72  val _ =
   29.73    OuterSyntax.command "code_module"
   29.74 -    "generates code for terms (single structure, incremental)" K.thy_decl
   29.75 +    "generates code for terms (single structure, incremental)" Keyword.thy_decl
   29.76      (parse_code false);
   29.77  
   29.78  end;