# HG changeset patch
# User wenzelm
# Date 1273958192 -7200
# Node ID 75b8f26f2f071254a970daf6d979989a58ac9082
# Parent  080e85d46108b4a1f2546586fe5f2e70d3336262
refer directly to structure Keyword and Parse;
eliminated old-style structure aliases K and P;

diff -r 080e85d46108 -r 75b8f26f2f07 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Isar/args.ML	Sat May 15 23:16:32 2010 +0200
@@ -71,7 +71,6 @@
 struct
 
 structure T = OuterLex;
-structure P = OuterParse;
 
 type token = T.token;
 
@@ -125,17 +124,17 @@
 
 (* basic *)
 
-fun token atom = Scan.ahead P.not_eof --| atom;
+fun token atom = Scan.ahead Parse.not_eof --| atom;
 
 val ident = token
-  (P.short_ident || P.long_ident || P.sym_ident || P.term_var ||
-    P.type_ident || P.type_var || P.number);
+  (Parse.short_ident || Parse.long_ident || Parse.sym_ident || Parse.term_var ||
+    Parse.type_ident || Parse.type_var || Parse.number);
 
-val string = token (P.string || P.verbatim);
-val alt_string = token P.alt_string;
-val symbolic = token P.keyword_ident_or_symbolic;
+val string = token (Parse.string || Parse.verbatim);
+val alt_string = token Parse.alt_string;
+val symbolic = token Parse.keyword_ident_or_symbolic;
 
-fun $$$ x = (ident >> T.content_of || P.keyword)
+fun $$$ x = (ident >> T.content_of || Parse.keyword)
   :|-- (fn y => if x = y then Scan.succeed x else Scan.fail);
 
 
@@ -158,7 +157,7 @@
 val name_source_position = named >> T.source_position_of;
 
 val name = named >> T.content_of;
-val binding = P.position name >> Binding.make;
+val binding = Parse.position name >> Binding.make;
 val alt_name = alt_string >> T.content_of;
 val symbol = symbolic >> T.content_of;
 val liberal_name = symbol || name;
@@ -216,12 +215,12 @@
 (* improper method arguments *)
 
 val from_to =
-  P.nat -- ($$$ "-" |-- P.nat) >> (fn (i, j) => fn tac => Seq.INTERVAL tac i j) ||
-  P.nat --| $$$ "-" >> (fn i => fn tac => fn st => Seq.INTERVAL tac i (Thm.nprems_of st) st) ||
-  P.nat >> (fn i => fn tac => tac i) ||
+  Parse.nat -- ($$$ "-" |-- Parse.nat) >> (fn (i, j) => fn tac => Seq.INTERVAL tac i j) ||
+  Parse.nat --| $$$ "-" >> (fn i => fn tac => fn st => Seq.INTERVAL tac i (Thm.nprems_of st) st) ||
+  Parse.nat >> (fn i => fn tac => tac i) ||
   $$$ "!" >> K ALLGOALS;
 
-val goal = $$$ "[" |-- P.!!! (from_to --| $$$ "]");
+val goal = $$$ "[" |-- Parse.!!! (from_to --| $$$ "]");
 fun goal_spec x = Scan.lift (Scan.optional goal (fn tac => tac 1)) x;
 
 
@@ -229,10 +228,10 @@
 
 fun parse_args is_symid =
   let
-    val keyword_symid = token (P.keyword_with is_symid);
-    fun atom blk = P.group "argument"
+    val keyword_symid = token (Parse.keyword_with is_symid);
+    fun atom blk = Parse.group "argument"
       (ident || keyword_symid || string || alt_string ||
-        (if blk then token (P.$$$ ",") else Scan.fail));
+        (if blk then token (Parse.$$$ ",") else Scan.fail));
 
     fun args blk x = Scan.optional (args1 blk) [] x
     and args1 blk x =
@@ -240,7 +239,8 @@
         (Scan.repeat1 (atom blk) ||
           argsp "(" ")" ||
           argsp "[" "]")) >> flat) x
-    and argsp l r x = (token (P.$$$ l) ::: P.!!! (args true @@@ (token (P.$$$ r) >> single))) x;
+    and argsp l r x =
+      (token (Parse.$$$ l) ::: Parse.!!! (args true @@@ (token (Parse.$$$ r) >> single))) x;
   in (args, args1) end;
 
 val parse = #1 (parse_args T.ident_or_symbolic) false;
@@ -253,8 +253,8 @@
   let
     val attrib_name = internal_text || (symbolic || named)
       >> evaluate T.Text (intern o T.content_of);
-    val attrib = P.position (attrib_name -- P.!!! parse) >> src;
-  in $$$ "[" |-- P.!!! (P.list attrib --| $$$ "]") end;
+    val attrib = Parse.position (attrib_name -- Parse.!!! parse) >> src;
+  in $$$ "[" |-- Parse.!!! (Parse.list attrib --| $$$ "]") end;
 
 fun opt_attribs intern = Scan.optional (attribs intern) [];
 
diff -r 080e85d46108 -r 75b8f26f2f07 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Isar/attrib.ML	Sat May 15 23:16:32 2010 +0200
@@ -48,7 +48,6 @@
 struct
 
 structure T = OuterLex;
-structure P = OuterParse;
 
 
 (* source and bindings *)
@@ -168,10 +167,10 @@
 
 (** parsing attributed theorems **)
 
-val thm_sel = P.$$$ "(" |-- P.list1
- (P.nat --| P.minus -- P.nat >> Facts.FromTo ||
-  P.nat --| P.minus >> Facts.From ||
-  P.nat >> Facts.Single) --| P.$$$ ")";
+val thm_sel = Parse.$$$ "(" |-- Parse.list1
+ (Parse.nat --| Parse.minus -- Parse.nat >> Facts.FromTo ||
+  Parse.nat --| Parse.minus >> Facts.From ||
+  Parse.nat >> Facts.Single) --| Parse.$$$ ")";
 
 local
 
@@ -184,7 +183,7 @@
     val get_fact = get o Facts.Fact;
     fun get_named pos name = get (Facts.Named ((name, pos), NONE));
   in
-    P.$$$ "[" |-- Args.attribs (intern thy) --| P.$$$ "]" >> (fn srcs =>
+    Parse.$$$ "[" |-- Args.attribs (intern thy) --| Parse.$$$ "]" >> (fn srcs =>
       let
         val atts = map (attribute_i thy) srcs;
         val (context', th') = Library.apply atts (context, Drule.dummy_thm);
@@ -192,7 +191,7 @@
     ||
     (Scan.ahead Args.alt_name -- Args.named_fact get_fact
       >> (fn (s, fact) => ("", Facts.Fact s, fact)) ||
-     Scan.ahead (P.position fact_name) :|-- (fn (name, pos) =>
+     Scan.ahead (Parse.position fact_name) :|-- (fn (name, pos) =>
       Args.named_fact (get_named pos) -- Scan.option thm_sel
         >> (fn (fact, sel) => (name, Facts.Named ((name, pos), sel), fact))))
     -- Args.opt_attribs (intern thy) >> (fn ((name, thmref, fact), srcs) =>
@@ -223,11 +222,11 @@
 (* rule composition *)
 
 val COMP_att =
-  Scan.lift (Scan.optional (Args.bracks P.nat) 1) -- thm
+  Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- thm
     >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => Drule.compose_single (A, i, B)));
 
 val THEN_att =
-  Scan.lift (Scan.optional (Args.bracks P.nat) 1) -- thm
+  Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- thm
     >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)));
 
 val OF_att =
@@ -267,7 +266,7 @@
 val eta_long =
   Thm.rule_attribute (K (Conv.fconv_rule Drule.eta_long_conversion));
 
-val rotated = Scan.optional P.int 1 >> (fn n => Thm.rule_attribute (K (rotate_prems n)));
+val rotated = Scan.optional Parse.int 1 >> (fn n => Thm.rule_attribute (K (rotate_prems n)));
 
 
 (* theory setup *)
@@ -285,9 +284,9 @@
     "rename bound variables in abstractions" #>
   setup (Binding.name "unfolded") unfolded "unfolded definitions" #>
   setup (Binding.name "folded") folded "folded definitions" #>
-  setup (Binding.name "consumes") (Scan.lift (Scan.optional P.nat 1) >> Rule_Cases.consumes)
+  setup (Binding.name "consumes") (Scan.lift (Scan.optional Parse.nat 1) >> Rule_Cases.consumes)
     "number of consumed facts" #>
-  setup (Binding.name "constraints") (Scan.lift P.nat >> Rule_Cases.constraints)
+  setup (Binding.name "constraints") (Scan.lift Parse.nat >> Rule_Cases.constraints)
     "number of equality constraints" #>
   setup (Binding.name "case_names") (Scan.lift (Scan.repeat1 Args.name) >> Rule_Cases.case_names)
     "named rule cases" #>
@@ -295,7 +294,7 @@
     (Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion)
     "named conclusion of rule cases" #>
   setup (Binding.name "params")
-    (Scan.lift (P.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params)
+    (Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params)
     "named rule parameters" #>
   setup (Binding.name "standard") (Scan.succeed (Thm.rule_attribute (K Drule.export_without_context)))
     "result put into standard form (legacy)" #>
@@ -345,13 +344,13 @@
 
 local
 
-val equals = P.$$$ "=";
+val equals = Parse.$$$ "=";
 
 fun scan_value (Config.Bool _) =
       equals -- Args.$$$ "false" >> K (Config.Bool false) ||
       equals -- Args.$$$ "true" >> K (Config.Bool true) ||
       Scan.succeed (Config.Bool true)
-  | scan_value (Config.Int _) = equals |-- P.int >> Config.Int
+  | scan_value (Config.Int _) = equals |-- Parse.int >> Config.Int
   | scan_value (Config.String _) = equals |-- Args.name >> Config.String;
 
 fun scan_config thy config =
diff -r 080e85d46108 -r 75b8f26f2f07 src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Isar/context_rules.ML	Sat May 15 23:16:32 2010 +0200
@@ -203,7 +203,7 @@
 
 fun add a b c x =
   (Scan.lift ((Args.bang >> K a || Args.query >> K c || Scan.succeed b) --
-    Scan.option OuterParse.nat) >> (fn (f, n) => f n)) x;
+    Scan.option Parse.nat) >> (fn (f, n) => f n)) x;
 
 val _ = Context.>> (Context.map_theory
  (Attrib.setup (Binding.name "intro") (add intro_bang intro intro_query)
diff -r 080e85d46108 -r 75b8f26f2f07 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sat May 15 23:16:32 2010 +0200
@@ -507,7 +507,7 @@
 
 fun check_text (txt, pos) state =
  (Position.report Markup.doc_source pos;
-  ignore (ThyOutput.eval_antiquote (#1 (OuterKeyword.get_lexicons ())) state (txt, pos)));
+  ignore (ThyOutput.eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));
 
 fun header_markup txt = Toplevel.keep (fn state =>
   if Toplevel.is_toplevel state then check_text txt state
diff -r 080e85d46108 -r 75b8f26f2f07 src/Pure/Isar/isar_document.ML
--- a/src/Pure/Isar/isar_document.ML	Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Isar/isar_document.ML	Sat May 15 23:16:32 2010 +0200
@@ -275,27 +275,28 @@
 
 (** concrete syntax **)
 
-local structure P = OuterParse structure V = ValueParse in
+local structure V = ValueParse in
 
 val _ =
   OuterSyntax.internal_command "Isar.define_command"
-    (P.string -- P.string >> (fn (id, text) =>
+    (Parse.string -- Parse.string >> (fn (id, text) =>
       Toplevel.position (Position.id_only id) o
       Toplevel.imperative (fn () =>
         define_command id (OuterSyntax.prepare_command (Position.id id) text))));
 
 val _ =
   OuterSyntax.internal_command "Isar.begin_document"
-    (P.string -- P.string >> (fn (id, path) =>
+    (Parse.string -- Parse.string >> (fn (id, path) =>
       Toplevel.imperative (fn () => begin_document id (Path.explode path))));
 
 val _ =
   OuterSyntax.internal_command "Isar.end_document"
-    (P.string >> (fn id => Toplevel.imperative (fn () => end_document id)));
+    (Parse.string >> (fn id => Toplevel.imperative (fn () => end_document id)));
 
 val _ =
   OuterSyntax.internal_command "Isar.edit_document"
-    (P.string -- P.string -- V.list (P.string -- (P.string >> SOME) || P.string >> rpair NONE)
+    (Parse.string -- Parse.string --
+        V.list (Parse.string -- (Parse.string >> SOME) || Parse.string >> rpair NONE)
       >> (fn ((id, new_id), edits) =>
         Toplevel.position (Position.id_only new_id) o
         Toplevel.imperative (fn () => edit_document id new_id edits)));
diff -r 080e85d46108 -r 75b8f26f2f07 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sat May 15 23:16:32 2010 +0200
@@ -7,15 +7,12 @@
 structure IsarSyn: sig end =
 struct
 
-structure P = OuterParse and K = OuterKeyword;
-
-
 (** keywords **)
 
 (*keep keywords consistent with the parsers, otherwise be prepared for
   unexpected errors*)
 
-val _ = List.app OuterKeyword.keyword
+val _ = List.app Keyword.keyword
  ["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
   "=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>",
   "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
@@ -30,54 +27,54 @@
 (** init and exit **)
 
 val _ =
-  OuterSyntax.command "theory" "begin theory" (K.tag_theory K.thy_begin)
+  OuterSyntax.command "theory" "begin theory" (Keyword.tag_theory Keyword.thy_begin)
     (Thy_Header.args >> (Toplevel.print oo IsarCmd.init_theory));
 
 val _ =
-  OuterSyntax.command "end" "end (local) theory" (K.tag_theory K.thy_end)
+  OuterSyntax.command "end" "end (local) theory" (Keyword.tag_theory Keyword.thy_end)
     (Scan.succeed (Toplevel.exit o Toplevel.end_local_theory));
 
 
 
 (** markup commands **)
 
-val _ = OuterSyntax.markup_command ThyOutput.Markup "header" "theory header" K.diag
-  (P.doc_source >> IsarCmd.header_markup);
+val _ = OuterSyntax.markup_command ThyOutput.Markup "header" "theory header" Keyword.diag
+  (Parse.doc_source >> IsarCmd.header_markup);
 
 val _ = OuterSyntax.markup_command ThyOutput.Markup "chapter" "chapter heading"
-  K.thy_heading (P.opt_target -- P.doc_source >> IsarCmd.local_theory_markup);
+  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
 
 val _ = OuterSyntax.markup_command ThyOutput.Markup "section" "section heading"
-  K.thy_heading (P.opt_target -- P.doc_source >> IsarCmd.local_theory_markup);
+  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
 
 val _ = OuterSyntax.markup_command ThyOutput.Markup "subsection" "subsection heading"
-  K.thy_heading (P.opt_target -- P.doc_source >> IsarCmd.local_theory_markup);
+  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
 
 val _ =
   OuterSyntax.markup_command ThyOutput.Markup "subsubsection" "subsubsection heading"
-  K.thy_heading (P.opt_target -- P.doc_source >> IsarCmd.local_theory_markup);
+  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
 
 val _ = OuterSyntax.markup_command ThyOutput.MarkupEnv "text" "formal comment (theory)"
-  K.thy_decl (P.opt_target -- P.doc_source >> IsarCmd.local_theory_markup);
+  Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
 
 val _ = OuterSyntax.markup_command ThyOutput.Verbatim "text_raw" "raw document preparation text"
-  K.thy_decl (P.opt_target -- P.doc_source >> IsarCmd.local_theory_markup);
+  Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
 
 val _ = OuterSyntax.markup_command ThyOutput.Markup "sect" "formal comment (proof)"
-  (K.tag_proof K.prf_heading) (P.doc_source >> IsarCmd.proof_markup);
+  (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> IsarCmd.proof_markup);
 
 val _ = OuterSyntax.markup_command ThyOutput.Markup "subsect" "formal comment (proof)"
-  (K.tag_proof K.prf_heading) (P.doc_source >> IsarCmd.proof_markup);
+  (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> IsarCmd.proof_markup);
 
 val _ = OuterSyntax.markup_command ThyOutput.Markup "subsubsect" "formal comment (proof)"
-  (K.tag_proof K.prf_heading) (P.doc_source >> IsarCmd.proof_markup);
+  (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> IsarCmd.proof_markup);
 
 val _ = OuterSyntax.markup_command ThyOutput.MarkupEnv "txt" "formal comment (proof)"
-  (K.tag_proof K.prf_decl) (P.doc_source >> IsarCmd.proof_markup);
+  (Keyword.tag_proof Keyword.prf_decl) (Parse.doc_source >> IsarCmd.proof_markup);
 
 val _ = OuterSyntax.markup_command ThyOutput.Verbatim "txt_raw"
-  "raw document preparation text (proof)" (K.tag_proof K.prf_decl)
-  (P.doc_source >> IsarCmd.proof_markup);
+  "raw document preparation text (proof)" (Keyword.tag_proof Keyword.prf_decl)
+  (Parse.doc_source >> IsarCmd.proof_markup);
 
 
 
@@ -86,175 +83,185 @@
 (* classes and sorts *)
 
 val _ =
-  OuterSyntax.command "classes" "declare type classes" K.thy_decl
-    (Scan.repeat1 (P.binding -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
-        P.!!! (P.list1 P.xname)) []) >> (Toplevel.theory o fold AxClass.axiomatize_class_cmd));
+  OuterSyntax.command "classes" "declare type classes" Keyword.thy_decl
+    (Scan.repeat1 (Parse.binding -- Scan.optional ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |--
+        Parse.!!! (Parse.list1 Parse.xname)) [])
+      >> (Toplevel.theory o fold AxClass.axiomatize_class_cmd));
 
 val _ =
-  OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl
-    (P.and_list1 (P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname))
+  OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" Keyword.thy_decl
+    (Parse.and_list1 (Parse.xname -- ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<")
+        |-- Parse.!!! Parse.xname))
     >> (Toplevel.theory o AxClass.axiomatize_classrel_cmd));
 
 val _ =
   OuterSyntax.local_theory "default_sort" "declare default sort for explicit type variables"
-    K.thy_decl
-    (P.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy));
+    Keyword.thy_decl
+    (Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy));
 
 
 (* types *)
 
 val _ =
-  OuterSyntax.local_theory "typedecl" "type declaration" K.thy_decl
-    (P.type_args -- P.binding -- P.opt_mixfix
+  OuterSyntax.local_theory "typedecl" "type declaration" Keyword.thy_decl
+    (Parse.type_args -- Parse.binding -- Parse.opt_mixfix
       >> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd));
 
 val _ =
-  OuterSyntax.local_theory "types" "declare type abbreviations" K.thy_decl
+  OuterSyntax.local_theory "types" "declare type abbreviations" Keyword.thy_decl
     (Scan.repeat1
-      (P.type_args -- P.binding -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_mixfix')))
+      (Parse.type_args -- Parse.binding --
+        (Parse.$$$ "=" |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix')))
       >> (fold (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs)));
 
 val _ =
   OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
-    K.thy_decl (Scan.repeat1 P.binding >> (Toplevel.theory o Sign.add_nonterminals));
+    Keyword.thy_decl (Scan.repeat1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals));
 
 val _ =
-  OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl
-    (Scan.repeat1 P.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity_cmd));
+  OuterSyntax.command "arities" "state type arities (axiomatic!)" Keyword.thy_decl
+    (Scan.repeat1 Parse.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity_cmd));
 
 
 (* consts and syntax *)
 
 val _ =
-  OuterSyntax.command "judgment" "declare object-logic judgment" K.thy_decl
-    (P.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
+  OuterSyntax.command "judgment" "declare object-logic judgment" Keyword.thy_decl
+    (Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
 
 val _ =
-  OuterSyntax.command "consts" "declare constants" K.thy_decl
-    (Scan.repeat1 P.const_binding >> (Toplevel.theory o Sign.add_consts));
+  OuterSyntax.command "consts" "declare constants" Keyword.thy_decl
+    (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts));
 
-val opt_overloaded = P.opt_keyword "overloaded";
+val opt_overloaded = Parse.opt_keyword "overloaded";
 
 val _ =
-  OuterSyntax.command "finalconsts" "declare constants as final" K.thy_decl
-    (opt_overloaded -- Scan.repeat1 P.term >> (uncurry (Toplevel.theory oo Theory.add_finals)));
+  OuterSyntax.command "finalconsts" "declare constants as final" Keyword.thy_decl
+    (opt_overloaded -- Scan.repeat1 Parse.term >> (uncurry (Toplevel.theory oo Theory.add_finals)));
 
 val mode_spec =
-  (P.$$$ "output" >> K ("", false)) || P.name -- Scan.optional (P.$$$ "output" >> K false) true;
+  (Parse.$$$ "output" >> K ("", false)) ||
+    Parse.name -- Scan.optional (Parse.$$$ "output" >> K false) true;
 
 val opt_mode =
-  Scan.optional (P.$$$ "(" |-- P.!!! (mode_spec --| P.$$$ ")")) Syntax.mode_default;
+  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (mode_spec --| Parse.$$$ ")")) Syntax.mode_default;
 
 val _ =
-  OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl
-    (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Sign.add_modesyntax));
+  OuterSyntax.command "syntax" "declare syntactic constants" Keyword.thy_decl
+    (opt_mode -- Scan.repeat1 Parse.const >> (Toplevel.theory o uncurry Sign.add_modesyntax));
 
 val _ =
-  OuterSyntax.command "no_syntax" "delete syntax declarations" K.thy_decl
-    (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Sign.del_modesyntax));
+  OuterSyntax.command "no_syntax" "delete syntax declarations" Keyword.thy_decl
+    (opt_mode -- Scan.repeat1 Parse.const >> (Toplevel.theory o uncurry Sign.del_modesyntax));
 
 
 (* translations *)
 
 val trans_pat =
-  Scan.optional (P.$$$ "(" |-- P.!!! (P.xname --| P.$$$ ")")) "logic" -- P.string;
+  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.xname --| Parse.$$$ ")")) "logic"
+    -- Parse.string;
 
 fun trans_arrow toks =
-  ((P.$$$ "\\<rightharpoonup>" || P.$$$ "=>") >> K Syntax.ParseRule ||
-    (P.$$$ "\\<leftharpoondown>" || P.$$$ "<=") >> K Syntax.PrintRule ||
-    (P.$$$ "\\<rightleftharpoons>" || P.$$$ "==") >> K Syntax.ParsePrintRule) toks;
+  ((Parse.$$$ "\\<rightharpoonup>" || Parse.$$$ "=>") >> K Syntax.ParseRule ||
+    (Parse.$$$ "\\<leftharpoondown>" || Parse.$$$ "<=") >> K Syntax.PrintRule ||
+    (Parse.$$$ "\\<rightleftharpoons>" || Parse.$$$ "==") >> K Syntax.ParsePrintRule) toks;
 
 val trans_line =
-  trans_pat -- P.!!! (trans_arrow -- trans_pat)
+  trans_pat -- Parse.!!! (trans_arrow -- trans_pat)
     >> (fn (left, (arr, right)) => arr (left, right));
 
 val _ =
-  OuterSyntax.command "translations" "declare syntax translation rules" K.thy_decl
+  OuterSyntax.command "translations" "declare syntax translation rules" Keyword.thy_decl
     (Scan.repeat1 trans_line >> (Toplevel.theory o Sign.add_trrules));
 
 val _ =
-  OuterSyntax.command "no_translations" "remove syntax translation rules" K.thy_decl
+  OuterSyntax.command "no_translations" "remove syntax translation rules" Keyword.thy_decl
     (Scan.repeat1 trans_line >> (Toplevel.theory o Sign.del_trrules));
 
 
 (* axioms and definitions *)
 
 val _ =
-  OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
+  OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" Keyword.thy_decl
     (Scan.repeat1 SpecParse.spec >>
       (Toplevel.theory o
         (IsarCmd.add_axioms o
           tap (fn _ => legacy_feature "Old 'axioms' command -- use 'axiomatization' instead"))));
 
 val opt_unchecked_overloaded =
-  Scan.optional (P.$$$ "(" |-- P.!!!
-    (((P.$$$ "unchecked" >> K true) -- Scan.optional (P.$$$ "overloaded" >> K true) false ||
-      P.$$$ "overloaded" >> K (false, true)) --| P.$$$ ")")) (false, false);
+  Scan.optional (Parse.$$$ "(" |-- Parse.!!!
+    (((Parse.$$$ "unchecked" >> K true) -- Scan.optional (Parse.$$$ "overloaded" >> K true) false ||
+      Parse.$$$ "overloaded" >> K (false, true)) --| Parse.$$$ ")")) (false, false);
 
 val _ =
-  OuterSyntax.command "defs" "define constants" K.thy_decl
+  OuterSyntax.command "defs" "define constants" Keyword.thy_decl
     (opt_unchecked_overloaded --
-      Scan.repeat1 (SpecParse.thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y)))
+      Scan.repeat1 (SpecParse.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y)))
       >> (Toplevel.theory o IsarCmd.add_defs));
 
 
 (* old constdefs *)
 
 val old_constdecl =
-  P.binding --| P.where_ >> (fn x => (x, NONE, NoSyn)) ||
-  P.binding -- (P.$$$ "::" |-- P.!!! P.typ >> SOME) -- P.opt_mixfix'
-    --| Scan.option P.where_ >> P.triple1 ||
-  P.binding -- (P.mixfix >> pair NONE) --| Scan.option P.where_ >> P.triple2;
+  Parse.binding --| Parse.where_ >> (fn x => (x, NONE, NoSyn)) ||
+  Parse.binding -- (Parse.$$$ "::" |-- Parse.!!! Parse.typ >> SOME) -- Parse.opt_mixfix'
+    --| Scan.option Parse.where_ >> Parse.triple1 ||
+  Parse.binding -- (Parse.mixfix >> pair NONE) --| Scan.option Parse.where_ >> Parse.triple2;
 
-val old_constdef = Scan.option old_constdecl -- (SpecParse.opt_thm_name ":" -- P.prop);
+val old_constdef = Scan.option old_constdecl -- (SpecParse.opt_thm_name ":" -- Parse.prop);
 
 val structs =
-  Scan.optional ((P.$$$ "(" -- P.$$$ "structure") |-- P.!!! (P.simple_fixes --| P.$$$ ")")) [];
+  Scan.optional ((Parse.$$$ "(" -- Parse.$$$ "structure")
+    |-- Parse.!!! (Parse.simple_fixes --| Parse.$$$ ")")) [];
 
 val _ =
-  OuterSyntax.command "constdefs" "old-style constant definition" K.thy_decl
+  OuterSyntax.command "constdefs" "old-style constant definition" Keyword.thy_decl
     (structs -- Scan.repeat1 old_constdef >> (Toplevel.theory o Constdefs.add_constdefs));
 
 
 (* constant definitions and abbreviations *)
 
 val _ =
-  OuterSyntax.local_theory "definition" "constant definition" K.thy_decl
+  OuterSyntax.local_theory "definition" "constant definition" Keyword.thy_decl
     (SpecParse.constdef >> (fn args => #2 o Specification.definition_cmd args));
 
 val _ =
-  OuterSyntax.local_theory "abbreviation" "constant abbreviation" K.thy_decl
-    (opt_mode -- (Scan.option SpecParse.constdecl -- P.prop)
-    >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
+  OuterSyntax.local_theory "abbreviation" "constant abbreviation" Keyword.thy_decl
+    (opt_mode -- (Scan.option SpecParse.constdecl -- Parse.prop)
+      >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
 
 val _ =
-  OuterSyntax.local_theory "type_notation" "add concrete syntax for type constructors" K.thy_decl
-    (opt_mode -- P.and_list1 (P.xname -- P.mixfix)
-    >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
+  OuterSyntax.local_theory "type_notation" "add concrete syntax for type constructors"
+    Keyword.thy_decl
+    (opt_mode -- Parse.and_list1 (Parse.xname -- Parse.mixfix)
+      >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
 
 val _ =
-  OuterSyntax.local_theory "no_type_notation" "delete concrete syntax for type constructors" K.thy_decl
-    (opt_mode -- P.and_list1 (P.xname -- P.mixfix)
-    >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
+  OuterSyntax.local_theory "no_type_notation" "delete concrete syntax for type constructors"
+    Keyword.thy_decl
+    (opt_mode -- Parse.and_list1 (Parse.xname -- Parse.mixfix)
+      >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
 
 val _ =
-  OuterSyntax.local_theory "notation" "add concrete syntax for constants / fixed variables" K.thy_decl
-    (opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
-    >> (fn (mode, args) => Specification.notation_cmd true mode args));
+  OuterSyntax.local_theory "notation" "add concrete syntax for constants / fixed variables"
+    Keyword.thy_decl
+    (opt_mode -- Parse.and_list1 (Parse.xname -- SpecParse.locale_mixfix)
+      >> (fn (mode, args) => Specification.notation_cmd true mode args));
 
 val _ =
-  OuterSyntax.local_theory "no_notation" "delete concrete syntax for constants / fixed variables" K.thy_decl
-    (opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
-    >> (fn (mode, args) => Specification.notation_cmd false mode args));
+  OuterSyntax.local_theory "no_notation" "delete concrete syntax for constants / fixed variables"
+    Keyword.thy_decl
+    (opt_mode -- Parse.and_list1 (Parse.xname -- SpecParse.locale_mixfix)
+      >> (fn (mode, args) => Specification.notation_cmd false mode args));
 
 
 (* constant specifications *)
 
 val _ =
-  OuterSyntax.command "axiomatization" "axiomatic constant specification" K.thy_decl
-    (Scan.optional P.fixes [] --
-      Scan.optional (P.where_ |-- P.!!! (P.and_list1 SpecParse.specs)) []
-    >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));
+  OuterSyntax.command "axiomatization" "axiomatic constant specification" Keyword.thy_decl
+    (Scan.optional Parse.fixes [] --
+      Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 SpecParse.specs)) []
+      >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));
 
 
 (* theorems *)
@@ -263,30 +270,30 @@
   SpecParse.name_facts >> (fn args => #2 o Specification.theorems_cmd kind args);
 
 val _ =
-  OuterSyntax.local_theory "theorems" "define theorems" K.thy_decl (theorems Thm.theoremK);
+  OuterSyntax.local_theory "theorems" "define theorems" Keyword.thy_decl (theorems Thm.theoremK);
 
 val _ =
-  OuterSyntax.local_theory "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK);
+  OuterSyntax.local_theory "lemmas" "define lemmas" Keyword.thy_decl (theorems Thm.lemmaK);
 
 val _ =
-  OuterSyntax.local_theory "declare" "declare theorems" K.thy_decl
-    (P.and_list1 SpecParse.xthms1
+  OuterSyntax.local_theory "declare" "declare theorems" Keyword.thy_decl
+    (Parse.and_list1 SpecParse.xthms1
       >> (fn args => #2 o Specification.theorems_cmd "" [(Attrib.empty_binding, flat args)]));
 
 
 (* name space entry path *)
 
 val _ =
-  OuterSyntax.command "global" "disable prefixing of theory name" K.thy_decl
+  OuterSyntax.command "global" "disable prefixing of theory name" Keyword.thy_decl
     (Scan.succeed (Toplevel.theory Sign.root_path));
 
 val _ =
-  OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl
+  OuterSyntax.command "local" "enable prefixing of theory name" Keyword.thy_decl
     (Scan.succeed (Toplevel.theory Sign.local_path));
 
 fun hide_names name hide what =
-  OuterSyntax.command name ("hide " ^ what ^ " from name space") K.thy_decl
-    ((P.opt_keyword "open" >> not) -- Scan.repeat1 P.xname >>
+  OuterSyntax.command name ("hide " ^ what ^ " from name space") Keyword.thy_decl
+    ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 Parse.xname >>
       (Toplevel.theory o uncurry hide));
 
 val _ = hide_names "hide_class" IsarCmd.hide_class "classes";
@@ -305,101 +312,104 @@
   (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf;
 
 val _ =
-  OuterSyntax.command "use" "ML text from file" (K.tag_ml K.thy_decl)
-    (P.path >> (fn path => Toplevel.generic_theory (ThyInfo.exec_file false path #> propagate_env)));
+  OuterSyntax.command "use" "ML text from file" (Keyword.tag_ml Keyword.thy_decl)
+    (Parse.path >>
+      (fn path => Toplevel.generic_theory (ThyInfo.exec_file false path #> propagate_env)));
 
 val _ =
-  OuterSyntax.command "ML" "ML text within theory or local theory" (K.tag_ml K.thy_decl)
-    (P.ML_source >> (fn (txt, pos) =>
+  OuterSyntax.command "ML" "ML text within theory or local theory"
+    (Keyword.tag_ml Keyword.thy_decl)
+    (Parse.ML_source >> (fn (txt, pos) =>
       Toplevel.generic_theory
         (ML_Context.exec (fn () => ML_Context.eval true pos txt) #> propagate_env)));
 
 val _ =
-  OuterSyntax.command "ML_prf" "ML text within proof" (K.tag_proof K.prf_decl)
-    (P.ML_source >> (fn (txt, pos) =>
+  OuterSyntax.command "ML_prf" "ML text within proof" (Keyword.tag_proof Keyword.prf_decl)
+    (Parse.ML_source >> (fn (txt, pos) =>
       Toplevel.proof (Proof.map_context (Context.proof_map
         (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf)));
 
 val _ =
-  OuterSyntax.command "ML_val" "diagnostic ML text" (K.tag_ml K.diag)
-    (P.ML_source >> IsarCmd.ml_diag true);
+  OuterSyntax.command "ML_val" "diagnostic ML text" (Keyword.tag_ml Keyword.diag)
+    (Parse.ML_source >> IsarCmd.ml_diag true);
 
 val _ =
-  OuterSyntax.command "ML_command" "diagnostic ML text (silent)" (K.tag_ml K.diag)
-    (P.ML_source >> (Toplevel.no_timing oo IsarCmd.ml_diag false));
+  OuterSyntax.command "ML_command" "diagnostic ML text (silent)" (Keyword.tag_ml Keyword.diag)
+    (Parse.ML_source >> (Toplevel.no_timing oo IsarCmd.ml_diag false));
 
 val _ =
-  OuterSyntax.command "setup" "ML theory setup" (K.tag_ml K.thy_decl)
-    (P.ML_source >> (Toplevel.theory o IsarCmd.global_setup));
+  OuterSyntax.command "setup" "ML theory setup" (Keyword.tag_ml Keyword.thy_decl)
+    (Parse.ML_source >> (Toplevel.theory o IsarCmd.global_setup));
 
 val _ =
-  OuterSyntax.local_theory "local_setup" "ML local theory setup" (K.tag_ml K.thy_decl)
-    (P.ML_source >> IsarCmd.local_setup);
+  OuterSyntax.local_theory "local_setup" "ML local theory setup" (Keyword.tag_ml Keyword.thy_decl)
+    (Parse.ML_source >> IsarCmd.local_setup);
 
 val _ =
-  OuterSyntax.command "attribute_setup" "define attribute in ML" (K.tag_ml K.thy_decl)
-    (P.position P.name -- P.!!! (P.$$$ "=" |-- P.ML_source -- P.text)
-    >> (fn (name, (txt, cmt)) => Toplevel.theory (Attrib.attribute_setup name txt cmt)));
+  OuterSyntax.command "attribute_setup" "define attribute in ML" (Keyword.tag_ml Keyword.thy_decl)
+    (Parse.position Parse.name -- Parse.!!! (Parse.$$$ "=" |-- Parse.ML_source -- Parse.text)
+      >> (fn (name, (txt, cmt)) => Toplevel.theory (Attrib.attribute_setup name txt cmt)));
 
 val _ =
-  OuterSyntax.command "method_setup" "define proof method in ML" (K.tag_ml K.thy_decl)
-    (P.position P.name -- P.!!! (P.$$$ "=" |-- P.ML_source -- P.text)
-    >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
+  OuterSyntax.command "method_setup" "define proof method in ML" (Keyword.tag_ml Keyword.thy_decl)
+    (Parse.position Parse.name -- Parse.!!! (Parse.$$$ "=" |-- Parse.ML_source -- Parse.text)
+      >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
 
 val _ =
-  OuterSyntax.local_theory "declaration" "generic ML declaration" (K.tag_ml K.thy_decl)
-    (P.opt_keyword "pervasive" -- P.ML_source >> uncurry IsarCmd.declaration);
+  OuterSyntax.local_theory "declaration" "generic ML declaration" (Keyword.tag_ml Keyword.thy_decl)
+    (Parse.opt_keyword "pervasive" -- Parse.ML_source >> uncurry IsarCmd.declaration);
 
 val _ =
-  OuterSyntax.local_theory "simproc_setup" "define simproc in ML" (K.tag_ml K.thy_decl)
-    (P.name -- (P.$$$ "(" |-- P.enum1 "|" P.term --| P.$$$ ")" --| P.$$$ "=") --
-      P.ML_source -- Scan.optional (P.$$$ "identifier" |-- Scan.repeat1 P.xname) []
+  OuterSyntax.local_theory "simproc_setup" "define simproc in ML" (Keyword.tag_ml Keyword.thy_decl)
+    (Parse.name --
+      (Parse.$$$ "(" |-- Parse.enum1 "|" Parse.term --| Parse.$$$ ")" --| Parse.$$$ "=") --
+      Parse.ML_source -- Scan.optional (Parse.$$$ "identifier" |-- Scan.repeat1 Parse.xname) []
     >> (fn (((a, b), c), d) => IsarCmd.simproc_setup a b c d));
 
 
 (* translation functions *)
 
-val trfun = P.opt_keyword "advanced" -- P.ML_source;
+val trfun = Parse.opt_keyword "advanced" -- Parse.ML_source;
 
 val _ =
   OuterSyntax.command "parse_ast_translation" "install parse ast translation functions"
-    (K.tag_ml K.thy_decl)
+    (Keyword.tag_ml Keyword.thy_decl)
     (trfun >> (Toplevel.theory o IsarCmd.parse_ast_translation));
 
 val _ =
   OuterSyntax.command "parse_translation" "install parse translation functions"
-    (K.tag_ml K.thy_decl)
+    (Keyword.tag_ml Keyword.thy_decl)
     (trfun >> (Toplevel.theory o IsarCmd.parse_translation));
 
 val _ =
   OuterSyntax.command "print_translation" "install print translation functions"
-    (K.tag_ml K.thy_decl)
+    (Keyword.tag_ml Keyword.thy_decl)
     (trfun >> (Toplevel.theory o IsarCmd.print_translation));
 
 val _ =
   OuterSyntax.command "typed_print_translation" "install typed print translation functions"
-    (K.tag_ml K.thy_decl)
+    (Keyword.tag_ml Keyword.thy_decl)
     (trfun >> (Toplevel.theory o IsarCmd.typed_print_translation));
 
 val _ =
   OuterSyntax.command "print_ast_translation" "install print ast translation functions"
-    (K.tag_ml K.thy_decl)
+    (Keyword.tag_ml Keyword.thy_decl)
     (trfun >> (Toplevel.theory o IsarCmd.print_ast_translation));
 
 
 (* oracles *)
 
 val _ =
-  OuterSyntax.command "oracle" "declare oracle" (K.tag_ml K.thy_decl)
-    (P.position P.name -- (P.$$$ "=" |-- P.ML_source) >>
+  OuterSyntax.command "oracle" "declare oracle" (Keyword.tag_ml Keyword.thy_decl)
+    (Parse.position Parse.name -- (Parse.$$$ "=" |-- Parse.ML_source) >>
       (fn (x, y) => Toplevel.theory (IsarCmd.oracle x y)));
 
 
 (* local theories *)
 
 val _ =
-  OuterSyntax.command "context" "enter local theory context" K.thy_decl
-    (P.name --| P.begin >> (fn name =>
+  OuterSyntax.command "context" "enter local theory context" Keyword.thy_decl
+    (Parse.name --| Parse.begin >> (fn name =>
       Toplevel.print o Toplevel.begin_local_theory true (Theory_Target.context_cmd name)));
 
 
@@ -407,36 +417,38 @@
 
 val locale_val =
   SpecParse.locale_expression false --
-    Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
+    Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
   Scan.repeat1 SpecParse.context_element >> pair ([], []);
 
 val _ =
-  OuterSyntax.command "locale" "define named proof context" K.thy_decl
-    (P.binding -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (([], []), []) -- P.opt_begin
+  OuterSyntax.command "locale" "define named proof context" Keyword.thy_decl
+    (Parse.binding --
+      Scan.optional (Parse.$$$ "=" |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
       >> (fn ((name, (expr, elems)), begin) =>
           (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
             (Expression.add_locale_cmd name Binding.empty expr elems #> snd)));
 
 val _ =
   OuterSyntax.command "sublocale"
-    "prove sublocale relation between a locale and a locale expression" K.thy_goal
-    (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! (SpecParse.locale_expression false)
+    "prove sublocale relation between a locale and a locale expression" Keyword.thy_goal
+    (Parse.xname --| (Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") --
+      Parse.!!! (SpecParse.locale_expression false)
       >> (fn (loc, expr) =>
           Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr)));
 
 val _ =
   OuterSyntax.command "interpretation"
-    "prove interpretation of locale expression in theory" K.thy_goal
-    (P.!!! (SpecParse.locale_expression true) --
-      Scan.optional (P.where_ |-- P.and_list1 (SpecParse.opt_thm_name ":" -- P.prop)) []
+    "prove interpretation of locale expression in theory" Keyword.thy_goal
+    (Parse.!!! (SpecParse.locale_expression true) --
+      Scan.optional (Parse.where_ |-- Parse.and_list1 (SpecParse.opt_thm_name ":" -- Parse.prop)) []
       >> (fn (expr, equations) => Toplevel.print o
           Toplevel.theory_to_proof (Expression.interpretation_cmd expr equations)));
 
 val _ =
   OuterSyntax.command "interpret"
     "prove interpretation of locale expression in proof context"
-    (K.tag_proof K.prf_goal)
-    (P.!!! (SpecParse.locale_expression true)
+    (Keyword.tag_proof Keyword.prf_goal)
+    (Parse.!!! (SpecParse.locale_expression true)
       >> (fn expr => Toplevel.print o Toplevel.proof' (Expression.interpret_cmd expr)));
 
 
@@ -444,41 +456,43 @@
 
 val class_val =
   SpecParse.class_expr --
-    Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
+    Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
   Scan.repeat1 SpecParse.context_element >> pair [];
 
 val _ =
-  OuterSyntax.command "class" "define type class" K.thy_decl
-   (P.binding -- Scan.optional (P.$$$ "=" |-- class_val) ([], []) -- P.opt_begin
+  OuterSyntax.command "class" "define type class" Keyword.thy_decl
+   (Parse.binding -- Scan.optional (Parse.$$$ "=" |-- class_val) ([], []) -- Parse.opt_begin
     >> (fn ((name, (supclasses, elems)), begin) =>
         (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
           (Class.class_cmd name supclasses elems #> snd)));
 
 val _ =
-  OuterSyntax.local_theory_to_proof "subclass" "prove a subclass relation" K.thy_goal
-    (P.xname >> Class.subclass_cmd);
+  OuterSyntax.local_theory_to_proof "subclass" "prove a subclass relation" Keyword.thy_goal
+    (Parse.xname >> Class.subclass_cmd);
 
 val _ =
-  OuterSyntax.command "instantiation" "instantiate and prove type arity" K.thy_decl
-   (P.multi_arity --| P.begin
+  OuterSyntax.command "instantiation" "instantiate and prove type arity" Keyword.thy_decl
+   (Parse.multi_arity --| Parse.begin
      >> (fn arities => Toplevel.print o
          Toplevel.begin_local_theory true (Theory_Target.instantiation_cmd arities)));
 
 val _ =
-  OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
-  ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> Class.classrel_cmd ||
-    P.multi_arity >> Class.instance_arity_cmd)
-    >> (Toplevel.print oo Toplevel.theory_to_proof)
-  || Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
+  OuterSyntax.command "instance" "prove type arity or subclass relation" Keyword.thy_goal
+  ((Parse.xname -- ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |-- Parse.!!! Parse.xname)
+        >> Class.classrel_cmd ||
+    Parse.multi_arity >> Class.instance_arity_cmd)
+    >> (Toplevel.print oo Toplevel.theory_to_proof) ||
+    Scan.succeed
+      (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
 
 
 (* arbitrary overloading *)
 
 val _ =
-  OuterSyntax.command "overloading" "overloaded definitions" K.thy_decl
-   (Scan.repeat1 (P.name --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.term --
-      Scan.optional (P.$$$ "(" |-- (P.$$$ "unchecked" >> K false) --| P.$$$ ")") true
-      >> P.triple1) --| P.begin
+  OuterSyntax.command "overloading" "overloaded definitions" Keyword.thy_decl
+   (Scan.repeat1 (Parse.name --| (Parse.$$$ "\\<equiv>" || Parse.$$$ "==") -- Parse.term --
+      Scan.optional (Parse.$$$ "(" |-- (Parse.$$$ "unchecked" >> K false) --| Parse.$$$ ")") true
+      >> Parse.triple1) --| Parse.begin
    >> (fn operations => Toplevel.print o
          Toplevel.begin_local_theory true (Theory_Target.overloading_cmd operations)));
 
@@ -486,8 +500,8 @@
 (* code generation *)
 
 val _ =
-  OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl
-    (Scan.repeat1 P.term >> (Toplevel.theory o Code.add_datatype_cmd));
+  OuterSyntax.command "code_datatype" "define set of code datatype constructors" Keyword.thy_decl
+    (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.add_datatype_cmd));
 
 
 
@@ -499,7 +513,7 @@
   OuterSyntax.local_theory_to_proof'
     (if schematic then "schematic_" ^ kind else kind)
     ("state " ^ (if schematic then "schematic " ^ kind else kind))
-    (if schematic then K.thy_schematic_goal else K.thy_goal)
+    (if schematic then Keyword.thy_schematic_goal else Keyword.thy_goal)
     (Scan.optional (SpecParse.opt_thm_name ":" --|
       Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) Attrib.empty_binding --
       SpecParse.general_statement >> (fn (a, (elems, concl)) =>
@@ -515,64 +529,64 @@
 
 val _ =
   OuterSyntax.local_theory_to_proof "example_proof"
-    "example proof body, without any result" K.thy_schematic_goal
+    "example proof body, without any result" Keyword.thy_schematic_goal
     (Scan.succeed
       (Specification.schematic_theorem_cmd "" NONE (K I)
         Attrib.empty_binding [] (Element.Shows []) false #> Proof.enter_forward));
 
 val _ =
   OuterSyntax.command "have" "state local goal"
-    (K.tag_proof K.prf_goal)
+    (Keyword.tag_proof Keyword.prf_goal)
     (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have));
 
 val _ =
   OuterSyntax.command "hence" "abbreviates \"then have\""
-    (K.tag_proof K.prf_goal)
+    (Keyword.tag_proof Keyword.prf_goal)
     (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.hence));
 
 val _ =
   OuterSyntax.command "show" "state local goal, solving current obligation"
-    (K.tag_proof K.prf_asm_goal)
+    (Keyword.tag_proof Keyword.prf_asm_goal)
     (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show));
 
 val _ =
   OuterSyntax.command "thus" "abbreviates \"then show\""
-    (K.tag_proof K.prf_asm_goal)
+    (Keyword.tag_proof Keyword.prf_asm_goal)
     (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus));
 
 
 (* facts *)
 
-val facts = P.and_list1 SpecParse.xthms1;
+val facts = Parse.and_list1 SpecParse.xthms1;
 
 val _ =
   OuterSyntax.command "then" "forward chaining"
-    (K.tag_proof K.prf_chain)
+    (Keyword.tag_proof Keyword.prf_chain)
     (Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain));
 
 val _ =
   OuterSyntax.command "from" "forward chaining from given facts"
-    (K.tag_proof K.prf_chain)
+    (Keyword.tag_proof Keyword.prf_chain)
     (facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss_cmd)));
 
 val _ =
   OuterSyntax.command "with" "forward chaining from given and current facts"
-    (K.tag_proof K.prf_chain)
+    (Keyword.tag_proof Keyword.prf_chain)
     (facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss_cmd)));
 
 val _ =
   OuterSyntax.command "note" "define facts"
-    (K.tag_proof K.prf_decl)
+    (Keyword.tag_proof Keyword.prf_decl)
     (SpecParse.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss_cmd)));
 
 val _ =
   OuterSyntax.command "using" "augment goal facts"
-    (K.tag_proof K.prf_decl)
+    (Keyword.tag_proof Keyword.prf_decl)
     (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using_cmd)));
 
 val _ =
   OuterSyntax.command "unfolding" "unfold definitions in goal and facts"
-    (K.tag_proof K.prf_decl)
+    (Keyword.tag_proof Keyword.prf_decl)
     (facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding_cmd)));
 
 
@@ -580,57 +594,59 @@
 
 val _ =
   OuterSyntax.command "fix" "fix local variables (Skolem constants)"
-    (K.tag_proof K.prf_asm)
-    (P.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix_cmd)));
+    (Keyword.tag_proof Keyword.prf_asm)
+    (Parse.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix_cmd)));
 
 val _ =
   OuterSyntax.command "assume" "assume propositions"
-    (K.tag_proof K.prf_asm)
+    (Keyword.tag_proof Keyword.prf_asm)
     (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume_cmd)));
 
 val _ =
   OuterSyntax.command "presume" "assume propositions, to be established later"
-    (K.tag_proof K.prf_asm)
+    (Keyword.tag_proof Keyword.prf_asm)
     (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd)));
 
 val _ =
   OuterSyntax.command "def" "local definition"
-    (K.tag_proof K.prf_asm)
-    (P.and_list1
+    (Keyword.tag_proof Keyword.prf_asm)
+    (Parse.and_list1
       (SpecParse.opt_thm_name ":" --
-        ((P.binding -- P.opt_mixfix) -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp)))
+        ((Parse.binding -- Parse.opt_mixfix) --
+          ((Parse.$$$ "\\<equiv>" || Parse.$$$ "==") |-- Parse.!!! Parse.termp)))
     >> (Toplevel.print oo (Toplevel.proof o Proof.def_cmd)));
 
 val _ =
   OuterSyntax.command "obtain" "generalized existence"
-    (K.tag_proof K.prf_asm_goal)
-    (P.parname -- Scan.optional (P.fixes --| P.where_) [] -- SpecParse.statement
+    (Keyword.tag_proof Keyword.prf_asm_goal)
+    (Parse.parname -- Scan.optional (Parse.fixes --| Parse.where_) [] -- SpecParse.statement
       >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain_cmd x y z)));
 
 val _ =
   OuterSyntax.command "guess" "wild guessing (unstructured)"
-    (K.tag_proof K.prf_asm_goal)
-    (Scan.optional P.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess_cmd)));
+    (Keyword.tag_proof Keyword.prf_asm_goal)
+    (Scan.optional Parse.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess_cmd)));
 
 val _ =
   OuterSyntax.command "let" "bind text variables"
-    (K.tag_proof K.prf_decl)
-    (P.and_list1 (P.and_list1 P.term -- (P.$$$ "=" |-- P.term))
+    (Keyword.tag_proof Keyword.prf_decl)
+    (Parse.and_list1 (Parse.and_list1 Parse.term -- (Parse.$$$ "=" |-- Parse.term))
       >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind_cmd)));
 
 val _ =
   OuterSyntax.command "write" "add concrete syntax for constants / fixed variables"
-    (K.tag_proof K.prf_decl)
-    (opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
+    (Keyword.tag_proof Keyword.prf_decl)
+    (opt_mode -- Parse.and_list1 (Parse.xname -- SpecParse.locale_mixfix)
     >> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args)));
 
 val case_spec =
-  (P.$$$ "(" |-- P.!!! (P.xname -- Scan.repeat1 (P.maybe P.name) --| P.$$$ ")") ||
-    P.xname >> rpair []) -- SpecParse.opt_attribs >> P.triple1;
+  (Parse.$$$ "(" |--
+    Parse.!!! (Parse.xname -- Scan.repeat1 (Parse.maybe Parse.name) --| Parse.$$$ ")") ||
+    Parse.xname >> rpair []) -- SpecParse.opt_attribs >> Parse.triple1;
 
 val _ =
   OuterSyntax.command "case" "invoke local context"
-    (K.tag_proof K.prf_asm)
+    (Keyword.tag_proof Keyword.prf_asm)
     (case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case_cmd)));
 
 
@@ -638,17 +654,17 @@
 
 val _ =
   OuterSyntax.command "{" "begin explicit proof block"
-    (K.tag_proof K.prf_open)
+    (Keyword.tag_proof Keyword.prf_open)
     (Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block));
 
 val _ =
   OuterSyntax.command "}" "end explicit proof block"
-    (K.tag_proof K.prf_close)
+    (Keyword.tag_proof Keyword.prf_close)
     (Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block));
 
 val _ =
   OuterSyntax.command "next" "enter next proof block"
-    (K.tag_proof K.prf_block)
+    (Keyword.tag_proof Keyword.prf_block)
     (Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block));
 
 
@@ -656,37 +672,37 @@
 
 val _ =
   OuterSyntax.command "qed" "conclude (sub-)proof"
-    (K.tag_proof K.qed_block)
+    (Keyword.tag_proof Keyword.qed_block)
     (Scan.option Method.parse >> IsarCmd.qed);
 
 val _ =
   OuterSyntax.command "by" "terminal backward proof"
-    (K.tag_proof K.qed)
+    (Keyword.tag_proof Keyword.qed)
     (Method.parse -- Scan.option Method.parse >> IsarCmd.terminal_proof);
 
 val _ =
   OuterSyntax.command ".." "default proof"
-    (K.tag_proof K.qed)
+    (Keyword.tag_proof Keyword.qed)
     (Scan.succeed IsarCmd.default_proof);
 
 val _ =
   OuterSyntax.command "." "immediate proof"
-    (K.tag_proof K.qed)
+    (Keyword.tag_proof Keyword.qed)
     (Scan.succeed IsarCmd.immediate_proof);
 
 val _ =
   OuterSyntax.command "done" "done proof"
-    (K.tag_proof K.qed)
+    (Keyword.tag_proof Keyword.qed)
     (Scan.succeed IsarCmd.done_proof);
 
 val _ =
   OuterSyntax.command "sorry" "skip proof (quick-and-dirty mode only!)"
-    (K.tag_proof K.qed)
+    (Keyword.tag_proof Keyword.qed)
     (Scan.succeed IsarCmd.skip_proof);
 
 val _ =
   OuterSyntax.command "oops" "forget proof"
-    (K.tag_proof K.qed_global)
+    (Keyword.tag_proof Keyword.qed_global)
     (Scan.succeed Toplevel.forget_proof);
 
 
@@ -694,27 +710,27 @@
 
 val _ =
   OuterSyntax.command "defer" "shuffle internal proof state"
-    (K.tag_proof K.prf_script)
-    (Scan.option P.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.defer)));
+    (Keyword.tag_proof Keyword.prf_script)
+    (Scan.option Parse.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.defer)));
 
 val _ =
   OuterSyntax.command "prefer" "shuffle internal proof state"
-    (K.tag_proof K.prf_script)
-    (P.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.prefer)));
+    (Keyword.tag_proof Keyword.prf_script)
+    (Parse.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.prefer)));
 
 val _ =
   OuterSyntax.command "apply" "initial refinement step (unstructured)"
-    (K.tag_proof K.prf_script)
+    (Keyword.tag_proof Keyword.prf_script)
     (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply)));
 
 val _ =
   OuterSyntax.command "apply_end" "terminal refinement (unstructured)"
-    (K.tag_proof K.prf_script)
+    (Keyword.tag_proof Keyword.prf_script)
     (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end)));
 
 val _ =
   OuterSyntax.command "proof" "backward proof"
-    (K.tag_proof K.prf_block)
+    (Keyword.tag_proof Keyword.prf_block)
     (Scan.option Method.parse >> (fn m => Toplevel.print o
       Toplevel.actual_proof (Proof_Node.applys (Proof.proof m)) o
       Toplevel.skip_proof (fn i => i + 1)));
@@ -723,26 +739,26 @@
 (* calculational proof commands *)
 
 val calc_args =
-  Scan.option (P.$$$ "(" |-- P.!!! ((SpecParse.xthms1 --| P.$$$ ")")));
+  Scan.option (Parse.$$$ "(" |-- Parse.!!! ((SpecParse.xthms1 --| Parse.$$$ ")")));
 
 val _ =
   OuterSyntax.command "also" "combine calculation and current facts"
-    (K.tag_proof K.prf_decl)
+    (Keyword.tag_proof Keyword.prf_decl)
     (calc_args >> (Toplevel.proofs' o Calculation.also_cmd));
 
 val _ =
   OuterSyntax.command "finally" "combine calculation and current facts, exhibit result"
-    (K.tag_proof K.prf_chain)
+    (Keyword.tag_proof Keyword.prf_chain)
     (calc_args >> (Toplevel.proofs' o Calculation.finally_cmd));
 
 val _ =
   OuterSyntax.command "moreover" "augment calculation by current facts"
-    (K.tag_proof K.prf_decl)
+    (Keyword.tag_proof Keyword.prf_decl)
     (Scan.succeed (Toplevel.proof' Calculation.moreover));
 
 val _ =
   OuterSyntax.command "ultimately" "augment calculation by current facts, exhibit result"
-    (K.tag_proof K.prf_chain)
+    (Keyword.tag_proof Keyword.prf_chain)
     (Scan.succeed (Toplevel.proof' Calculation.ultimately));
 
 
@@ -750,18 +766,19 @@
 
 val _ =
   OuterSyntax.command "back" "backtracking of proof command"
-    (K.tag_proof K.prf_script)
+    (Keyword.tag_proof Keyword.prf_script)
     (Scan.succeed (Toplevel.print o Toplevel.actual_proof Proof_Node.back o Toplevel.skip_proof I));
 
 
 (* nested commands *)
 
 val props_text =
-  Scan.optional ValueParse.properties [] -- P.position P.string >> (fn (props, (str, pos)) =>
-    (Position.of_properties (Position.default_properties pos props), str));
+  Scan.optional ValueParse.properties [] -- Parse.position Parse.string
+  >> (fn (props, (str, pos)) =>
+      (Position.of_properties (Position.default_properties pos props), str));
 
 val _ =
-  OuterSyntax.improper_command "Isabelle.command" "nested Isabelle command" K.control
+  OuterSyntax.improper_command "Isabelle.command" "nested Isabelle command" Keyword.control
     (props_text :|-- (fn (pos, str) =>
       (case OuterSyntax.parse pos str of
         [tr] => Scan.succeed (K tr)
@@ -772,151 +789,153 @@
 
 (** diagnostic commands (for interactive mode only) **)
 
-val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
-val opt_bang = Scan.optional (P.$$$ "!" >> K true) false;
+val opt_modes =
+  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
+
+val opt_bang = Scan.optional (Parse.$$$ "!" >> K true) false;
 
 val _ =
   OuterSyntax.improper_command "pretty_setmargin" "change default margin for pretty printing"
-    K.diag (P.nat >> (Toplevel.no_timing oo IsarCmd.pretty_setmargin));
+    Keyword.diag (Parse.nat >> (Toplevel.no_timing oo IsarCmd.pretty_setmargin));
 
 val _ =
-  OuterSyntax.improper_command "help" "print outer syntax commands" K.diag
+  OuterSyntax.improper_command "help" "print outer syntax commands" Keyword.diag
     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative OuterSyntax.print_outer_syntax));
 
 val _ =
-  OuterSyntax.improper_command "print_commands" "print outer syntax commands" K.diag
+  OuterSyntax.improper_command "print_commands" "print outer syntax commands" Keyword.diag
     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative OuterSyntax.print_outer_syntax));
 
 val _ =
-  OuterSyntax.improper_command "print_configs" "print configuration options" K.diag
+  OuterSyntax.improper_command "print_configs" "print configuration options" Keyword.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_configs));
 
 val _ =
-  OuterSyntax.improper_command "print_context" "print theory context name" K.diag
+  OuterSyntax.improper_command "print_context" "print theory context name" Keyword.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_context));
 
 val _ =
-  OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag
-    (opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theory));
+  OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)"
+    Keyword.diag (opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theory));
 
 val _ =
-  OuterSyntax.improper_command "print_syntax" "print inner syntax of context (verbose!)" K.diag
-    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax));
+  OuterSyntax.improper_command "print_syntax" "print inner syntax of context (verbose!)"
+    Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax));
 
 val _ =
-  OuterSyntax.improper_command "print_abbrevs" "print constant abbreviation of context" K.diag
-    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_abbrevs));
+  OuterSyntax.improper_command "print_abbrevs" "print constant abbreviation of context"
+    Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.print_abbrevs));
 
 val _ =
   OuterSyntax.improper_command "print_theorems"
-      "print theorems of local theory or proof context" K.diag
+      "print theorems of local theory or proof context" Keyword.diag
     (opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theorems));
 
 val _ =
-  OuterSyntax.improper_command "print_locales" "print locales of this theory" K.diag
+  OuterSyntax.improper_command "print_locales" "print locales of this theory" Keyword.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_locales));
 
 val _ =
-  OuterSyntax.improper_command "print_classes" "print classes of this theory" K.diag
+  OuterSyntax.improper_command "print_classes" "print classes of this theory" Keyword.diag
     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory
       o Toplevel.keep (Class.print_classes o Toplevel.theory_of)));
 
 val _ =
-  OuterSyntax.improper_command "print_locale" "print locale of this theory" K.diag
-    (opt_bang -- P.xname >> (Toplevel.no_timing oo IsarCmd.print_locale));
+  OuterSyntax.improper_command "print_locale" "print locale of this theory" Keyword.diag
+    (opt_bang -- Parse.xname >> (Toplevel.no_timing oo IsarCmd.print_locale));
 
 val _ =
   OuterSyntax.improper_command "print_interps"
-    "print interpretations of locale for this theory" K.diag
-    (P.xname >> (Toplevel.no_timing oo IsarCmd.print_registrations));
+    "print interpretations of locale for this theory" Keyword.diag
+    (Parse.xname >> (Toplevel.no_timing oo IsarCmd.print_registrations));
 
 val _ =
-  OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag
+  OuterSyntax.improper_command "print_attributes" "print attributes of this theory" Keyword.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes));
 
 val _ =
-  OuterSyntax.improper_command "print_simpset" "print context of Simplifier" K.diag
+  OuterSyntax.improper_command "print_simpset" "print context of Simplifier" Keyword.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_simpset));
 
 val _ =
-  OuterSyntax.improper_command "print_rules" "print intro/elim rules" K.diag
+  OuterSyntax.improper_command "print_rules" "print intro/elim rules" Keyword.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_rules));
 
 val _ =
-  OuterSyntax.improper_command "print_trans_rules" "print transitivity rules" K.diag
+  OuterSyntax.improper_command "print_trans_rules" "print transitivity rules" Keyword.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_trans_rules));
 
 val _ =
-  OuterSyntax.improper_command "print_methods" "print methods of this theory" K.diag
+  OuterSyntax.improper_command "print_methods" "print methods of this theory" Keyword.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_methods));
 
 val _ =
-  OuterSyntax.improper_command "print_antiquotations" "print antiquotations (global)" K.diag
+  OuterSyntax.improper_command "print_antiquotations" "print antiquotations (global)" Keyword.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations));
 
 val _ =
   OuterSyntax.improper_command "thy_deps" "visualize theory dependencies"
-    K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.thy_deps));
+    Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.thy_deps));
 
 val _ =
   OuterSyntax.improper_command "class_deps" "visualize class dependencies"
-    K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.class_deps));
+    Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.class_deps));
 
 val _ =
   OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies"
-    K.diag (SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
+    Keyword.diag (SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
 
 val _ =
-  OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag
+  OuterSyntax.improper_command "print_binds" "print term bindings of proof context" Keyword.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds));
 
 val _ =
-  OuterSyntax.improper_command "print_facts" "print facts of proof context" K.diag
+  OuterSyntax.improper_command "print_facts" "print facts of proof context" Keyword.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_facts));
 
 val _ =
-  OuterSyntax.improper_command "print_cases" "print cases of proof context" K.diag
+  OuterSyntax.improper_command "print_cases" "print cases of proof context" Keyword.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases));
 
 val _ =
-  OuterSyntax.improper_command "print_statement" "print theorems as long statements" K.diag
+  OuterSyntax.improper_command "print_statement" "print theorems as long statements" Keyword.diag
     (opt_modes -- SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts));
 
 val _ =
-  OuterSyntax.improper_command "thm" "print theorems" K.diag
+  OuterSyntax.improper_command "thm" "print theorems" Keyword.diag
     (opt_modes -- SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms));
 
 val _ =
-  OuterSyntax.improper_command "prf" "print proof terms of theorems" K.diag
+  OuterSyntax.improper_command "prf" "print proof terms of theorems" Keyword.diag
     (opt_modes -- Scan.option SpecParse.xthms1
       >> (Toplevel.no_timing oo IsarCmd.print_prfs false));
 
 val _ =
-  OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" K.diag
+  OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" Keyword.diag
     (opt_modes -- Scan.option SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs true));
 
 val _ =
-  OuterSyntax.improper_command "prop" "read and print proposition" K.diag
-    (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_prop));
+  OuterSyntax.improper_command "prop" "read and print proposition" Keyword.diag
+    (opt_modes -- Parse.term >> (Toplevel.no_timing oo IsarCmd.print_prop));
 
 val _ =
-  OuterSyntax.improper_command "term" "read and print term" K.diag
-    (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_term));
+  OuterSyntax.improper_command "term" "read and print term" Keyword.diag
+    (opt_modes -- Parse.term >> (Toplevel.no_timing oo IsarCmd.print_term));
 
 val _ =
-  OuterSyntax.improper_command "typ" "read and print type" K.diag
-    (opt_modes -- P.typ >> (Toplevel.no_timing oo IsarCmd.print_type));
+  OuterSyntax.improper_command "typ" "read and print type" Keyword.diag
+    (opt_modes -- Parse.typ >> (Toplevel.no_timing oo IsarCmd.print_type));
 
 val _ =
-  OuterSyntax.improper_command "print_codesetup" "print code generator setup" K.diag
+  OuterSyntax.improper_command "print_codesetup" "print code generator setup" Keyword.diag
     (Scan.succeed
       (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
         (Code.print_codesetup o Toplevel.theory_of)));
 
 val _ =
-  OuterSyntax.improper_command "unused_thms" "find unused theorems" K.diag
-    (Scan.option ((Scan.repeat1 (Scan.unless P.minus P.name) --| P.minus) --
-       Scan.option (Scan.repeat1 (Scan.unless P.minus P.name))) >>
+  OuterSyntax.improper_command "unused_thms" "find unused theorems" Keyword.diag
+    (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
+       Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >>
          (Toplevel.no_timing oo IsarCmd.unused_thms));
 
 
@@ -924,66 +943,66 @@
 (** system commands (for interactive mode only) **)
 
 val _ =
-  OuterSyntax.improper_command "cd" "change current working directory" K.diag
-    (P.path >> (Toplevel.no_timing oo IsarCmd.cd));
+  OuterSyntax.improper_command "cd" "change current working directory" Keyword.diag
+    (Parse.path >> (Toplevel.no_timing oo IsarCmd.cd));
 
 val _ =
-  OuterSyntax.improper_command "pwd" "print current working directory" K.diag
+  OuterSyntax.improper_command "pwd" "print current working directory" Keyword.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.pwd));
 
 val _ =
-  OuterSyntax.improper_command "use_thy" "use theory file" K.diag
-    (P.name >> (fn name =>
+  OuterSyntax.improper_command "use_thy" "use theory file" Keyword.diag
+    (Parse.name >> (fn name =>
       Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.use_thy name)));
 
 val _ =
-  OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag
-    (P.name >> (fn name =>
+  OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" Keyword.diag
+    (Parse.name >> (fn name =>
       Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.touch_thy name)));
 
 val _ =
-  OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag
-    (P.name >> (fn name =>
+  OuterSyntax.improper_command "remove_thy" "remove theory from loader database" Keyword.diag
+    (Parse.name >> (fn name =>
       Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.remove_thy name)));
 
 val _ =
   OuterSyntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"
-    K.diag (P.name >> (fn name =>
+    Keyword.diag (Parse.name >> (fn name =>
       Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.kill_thy name)));
 
 val _ =
   OuterSyntax.improper_command "display_drafts" "display raw source files with symbols"
-    K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.display_drafts));
+    Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo IsarCmd.display_drafts));
 
 val _ =
   OuterSyntax.improper_command "print_drafts" "print raw source files with symbols"
-    K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.print_drafts));
+    Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo IsarCmd.print_drafts));
 
 val opt_limits =
-  Scan.option P.nat -- Scan.option (P.$$$ "," |-- P.!!! P.nat);
+  Scan.option Parse.nat -- Scan.option (Parse.$$$ "," |-- Parse.!!! Parse.nat);
 
 val _ =
-  OuterSyntax.improper_command "pr" "print current proof state (if present)" K.diag
+  OuterSyntax.improper_command "pr" "print current proof state (if present)" Keyword.diag
     (opt_modes -- opt_limits >> (Toplevel.no_timing oo IsarCmd.pr));
 
 val _ =
-  OuterSyntax.improper_command "disable_pr" "disable printing of toplevel state" K.diag
+  OuterSyntax.improper_command "disable_pr" "disable printing of toplevel state" Keyword.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.disable_pr));
 
 val _ =
-  OuterSyntax.improper_command "enable_pr" "enable printing of toplevel state" K.diag
+  OuterSyntax.improper_command "enable_pr" "enable printing of toplevel state" Keyword.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.enable_pr));
 
 val _ =
-  OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag
-    (P.opt_unit >> K (Toplevel.no_timing o Toplevel.imperative Secure.commit));
+  OuterSyntax.improper_command "commit" "commit current session to ML database" Keyword.diag
+    (Parse.opt_unit >> K (Toplevel.no_timing o Toplevel.imperative Secure.commit));
 
 val _ =
-  OuterSyntax.improper_command "quit" "quit Isabelle" K.control
-    (P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit));
+  OuterSyntax.improper_command "quit" "quit Isabelle" Keyword.control
+    (Parse.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit));
 
 val _ =
-  OuterSyntax.improper_command "exit" "exit Isar loop" K.control
+  OuterSyntax.improper_command "exit" "exit Isar loop" Keyword.control
     (Scan.succeed (Toplevel.no_timing o IsarCmd.exit));
 
 end;
diff -r 080e85d46108 -r 75b8f26f2f07 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Isar/method.ML	Sat May 15 23:16:32 2010 +0200
@@ -382,9 +382,6 @@
 
 (** concrete syntax **)
 
-structure P = OuterParse;
-
-
 (* sections *)
 
 type modifier = (Proof.context -> Proof.context) * attribute;
@@ -407,7 +404,7 @@
 (* extra rule methods *)
 
 fun xrule_meth m =
-  Scan.lift (Scan.optional (Args.parens OuterParse.nat) 0) -- Attrib.thms >>
+  Scan.lift (Scan.optional (Args.parens Parse.nat) 0) -- Attrib.thms >>
   (fn (n, ths) => K (m n ths));
 
 
@@ -419,18 +416,18 @@
 local
 
 fun meth4 x =
- (P.position (P.xname >> rpair []) >> (Source o Args.src) ||
-  P.$$$ "(" |-- P.!!! (meth0 --| P.$$$ ")")) x
+ (Parse.position (Parse.xname >> rpair []) >> (Source o Args.src) ||
+  Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x
 and meth3 x =
- (meth4 --| P.$$$ "?" >> Try ||
-  meth4 --| P.$$$ "+" >> Repeat1 ||
-  meth4 -- (P.$$$ "[" |-- Scan.optional P.nat 1 --| P.$$$ "]") >> (SelectGoals o swap) ||
+ (meth4 --| Parse.$$$ "?" >> Try ||
+  meth4 --| Parse.$$$ "+" >> Repeat1 ||
+  meth4 -- (Parse.$$$ "[" |-- Scan.optional Parse.nat 1 --| Parse.$$$ "]") >> (SelectGoals o swap) ||
   meth4) x
 and meth2 x =
- (P.position (P.xname -- Args.parse1 is_symid_meth) >> (Source o Args.src) ||
+ (Parse.position (Parse.xname -- Args.parse1 is_symid_meth) >> (Source o Args.src) ||
   meth3) x
-and meth1 x = (P.enum1 "," meth2 >> (fn [m] => m | ms => Then ms)) x
-and meth0 x = (P.enum1 "|" meth1 >> (fn [m] => m | ms => Orelse ms)) x;
+and meth1 x = (Parse.enum1 "," meth2 >> (fn [m] => m | ms => Then ms)) x
+and meth0 x = (Parse.enum1 "|" meth1 >> (fn [m] => m | ms => Orelse ms)) x;
 
 in val parse = meth3 end;
 
@@ -463,12 +460,12 @@
   setup (Binding.name "rename_tac") (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name) >>
     (fn (quant, xs) => K (SIMPLE_METHOD'' quant (Tactic.rename_tac xs))))
     "rename parameters of goal" #>
-  setup (Binding.name "rotate_tac") (Args.goal_spec -- Scan.lift (Scan.optional P.int 1) >>
+  setup (Binding.name "rotate_tac") (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >>
     (fn (quant, i) => K (SIMPLE_METHOD'' quant (Tactic.rotate_tac i))))
       "rotate assumptions of goal" #>
-  setup (Binding.name "tactic") (Scan.lift (P.position Args.name) >> tactic)
+  setup (Binding.name "tactic") (Scan.lift (Parse.position Args.name) >> tactic)
     "ML tactic as proof method" #>
-  setup (Binding.name "raw_tactic") (Scan.lift (P.position Args.name) >> raw_tactic)
+  setup (Binding.name "raw_tactic") (Scan.lift (Parse.position Args.name) >> raw_tactic)
     "ML tactic as raw proof method"));
 
 
diff -r 080e85d46108 -r 75b8f26f2f07 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Sat May 15 23:16:32 2010 +0200
@@ -9,20 +9,20 @@
 
 signature OUTER_SYNTAX =
 sig
-  val command: string -> string -> OuterKeyword.T ->
+  val command: string -> string -> Keyword.T ->
     (Toplevel.transition -> Toplevel.transition) parser -> unit
-  val markup_command: ThyOutput.markup -> string -> string -> OuterKeyword.T ->
+  val markup_command: ThyOutput.markup -> string -> string -> Keyword.T ->
     (Toplevel.transition -> Toplevel.transition) parser -> unit
-  val improper_command: string -> string -> OuterKeyword.T ->
+  val improper_command: string -> string -> Keyword.T ->
     (Toplevel.transition -> Toplevel.transition) parser -> unit
   val internal_command: string -> (Toplevel.transition -> Toplevel.transition) parser -> unit
-  val local_theory': string -> string -> OuterKeyword.T ->
+  val local_theory': string -> string -> Keyword.T ->
     (bool -> local_theory -> local_theory) parser -> unit
-  val local_theory: string -> string -> OuterKeyword.T ->
+  val local_theory: string -> string -> Keyword.T ->
     (local_theory -> local_theory) parser -> unit
-  val local_theory_to_proof': string -> string -> OuterKeyword.T ->
+  val local_theory_to_proof': string -> string -> Keyword.T ->
     (bool -> local_theory -> Proof.state) parser -> unit
-  val local_theory_to_proof: string -> string -> OuterKeyword.T ->
+  val local_theory_to_proof: string -> string -> Keyword.T ->
     (local_theory -> Proof.state) parser -> unit
   val print_outer_syntax: unit -> unit
   val scan: Position.T -> string -> OuterLex.token list
@@ -38,8 +38,7 @@
 struct
 
 structure T = OuterLex;
-structure P = OuterParse;
-type 'a parser = 'a P.parser;
+type 'a parser = 'a Parse.parser;
 
 
 
@@ -62,20 +61,20 @@
 local
 
 fun terminate false = Scan.succeed ()
-  | terminate true = P.group "end of input" (Scan.option P.sync -- P.semicolon >> K ());
+  | terminate true = Parse.group "end of input" (Scan.option Parse.sync -- Parse.semicolon >> K ());
 
 fun body cmd (name, _) =
   (case cmd name of
     SOME (Command {int_only, parse, ...}) =>
-      P.!!! (Scan.prompt (name ^ "# ") (P.tags |-- parse >> pair int_only))
+      Parse.!!! (Scan.prompt (name ^ "# ") (Parse.tags |-- parse >> pair int_only))
   | NONE => sys_error ("no parser for outer syntax command " ^ quote name));
 
 in
 
 fun parse_command do_terminate cmd =
-  P.semicolon >> K NONE ||
-  P.sync >> K NONE ||
-  (P.position P.command :-- body cmd) --| terminate do_terminate
+  Parse.semicolon >> K NONE ||
+  Parse.sync >> K NONE ||
+  (Parse.position Parse.command :-- body cmd) --| terminate do_terminate
     >> (fn ((name, pos), (int_only, f)) =>
       SOME (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |>
         Toplevel.interactive int_only |> f));
@@ -105,7 +104,7 @@
 fun get_markups () = ! global_markups;
 
 fun get_command () = Symtab.lookup (get_commands ());
-fun get_syntax () = CRITICAL (fn () => (OuterKeyword.get_lexicons (), get_command ()));
+fun get_syntax () = CRITICAL (fn () => (Keyword.get_lexicons (), get_command ()));
 
 fun is_markup kind name = AList.lookup (op =) (get_markups ()) name = SOME kind;
 
@@ -113,7 +112,7 @@
 (* augment syntax *)
 
 fun add_command name kind cmd = CRITICAL (fn () =>
- (OuterKeyword.command name kind;
+ (Keyword.command name kind;
   if not (Symtab.defined (get_commands ()) name) then ()
   else warning ("Redefining outer syntax command " ^ quote name);
   change_commands (Symtab.update (name, cmd))));
@@ -130,13 +129,13 @@
 end;
 
 fun internal_command name parse =
-  command name "(internal)" OuterKeyword.control (parse >> (fn tr => Toplevel.no_timing o tr));
+  command name "(internal)" Keyword.control (parse >> (fn tr => Toplevel.no_timing o tr));
 
 
 (* local_theory commands *)
 
 fun local_theory_command do_print trans name comment kind parse =
-  command name comment kind (P.opt_target -- parse
+  command name comment kind (Parse.opt_target -- parse
     >> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f));
 
 val local_theory' = local_theory_command false Toplevel.local_theory';
@@ -157,7 +156,7 @@
       Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
     val (int_cmds, cmds) = List.partition #3 (dest_commands ());
   in
-    [Pretty.strs ("syntax keywords:" :: map quote (OuterKeyword.dest_keywords ())),
+    [Pretty.strs ("syntax keywords:" :: map quote (Keyword.dest_keywords ())),
       Pretty.big_list "commands:" (map pretty_cmd cmds),
       Pretty.big_list "interactive-only commands:" (map pretty_cmd int_cmds)]
     |> Pretty.chunks |> Pretty.writeln
@@ -172,18 +171,18 @@
 fun toplevel_source term do_recover cmd src =
   let
     val no_terminator =
-      Scan.unless P.semicolon (Scan.one (T.not_sync andf T.not_eof));
+      Scan.unless Parse.semicolon (Scan.one (T.not_sync andf T.not_eof));
     fun recover int =
       (int, fn _ => Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]);
   in
     src
     |> T.source_proper
     |> Source.source T.stopper
-      (Scan.bulk (P.$$$ "--" -- P.!!! P.doc_source >> K NONE || P.not_eof >> SOME))
+      (Scan.bulk (Parse.$$$ "--" -- Parse.!!! Parse.doc_source >> K NONE || Parse.not_eof >> SOME))
         (Option.map recover do_recover)
     |> Source.map_filter I
     |> Source.source T.stopper
-        (Scan.bulk (fn xs => P.!!! (parse_command term (cmd ())) xs))
+        (Scan.bulk (fn xs => Parse.!!! (parse_command term (cmd ())) xs))
         (Option.map recover do_recover)
     |> Source.map_filter I
   end;
@@ -194,13 +193,13 @@
 fun scan pos str =
   Source.of_string str
   |> Symbol.source {do_recover = false}
-  |> T.source {do_recover = SOME false} OuterKeyword.get_lexicons pos
+  |> T.source {do_recover = SOME false} Keyword.get_lexicons pos
   |> Source.exhaust;
 
 fun parse pos str =
   Source.of_string str
   |> Symbol.source {do_recover = false}
-  |> T.source {do_recover = SOME false} OuterKeyword.get_lexicons pos
+  |> T.source {do_recover = SOME false} Keyword.get_lexicons pos
   |> toplevel_source false NONE get_command
   |> Source.exhaust;
 
@@ -231,7 +230,7 @@
 fun isar term : isar =
   Source.tty
   |> Symbol.source {do_recover = true}
-  |> T.source {do_recover = SOME true} OuterKeyword.get_lexicons Position.none
+  |> T.source {do_recover = SOME true} Keyword.get_lexicons Position.none
   |> toplevel_source term (SOME true) get_command;
 
 
@@ -291,7 +290,7 @@
     val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
 
     fun after_load () =
-      ThyOutput.present_thy (#1 lexs) OuterKeyword.command_tags is_markup (Lazy.force results) toks
+      ThyOutput.present_thy (#1 lexs) Keyword.command_tags is_markup (Lazy.force results) toks
       |> Buffer.content
       |> Present.theory_output name;
   in after_load end;
diff -r 080e85d46108 -r 75b8f26f2f07 src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Isar/rule_insts.ML	Sat May 15 23:16:32 2010 +0200
@@ -30,7 +30,6 @@
 struct
 
 structure T = OuterLex;
-structure P = OuterParse;
 
 
 (** reading instantiations **)
@@ -215,14 +214,14 @@
   Args.internal_term >> T.Term ||
   Args.name_source >> T.Text;
 
-val inst = Args.var -- (Args.$$$ "=" |-- Scan.ahead P.not_eof -- value)
+val inst = Args.var -- (Args.$$$ "=" |-- Scan.ahead Parse.not_eof -- value)
   >> (fn (xi, (a, v)) => (a, (xi, v)));
 
 in
 
 val _ = Context.>> (Context.map_theory
   (Attrib.setup (Binding.name "where")
-    (Scan.lift (P.and_list inst) >> (fn args =>
+    (Scan.lift (Parse.and_list inst) >> (fn args =>
       Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)))
     "named instantiation of theorem"));
 
@@ -237,7 +236,7 @@
   Args.internal_term >> T.Term ||
   Args.name_source >> T.Text;
 
-val inst = Scan.ahead P.not_eof -- Args.maybe value;
+val inst = Scan.ahead Parse.not_eof -- Args.maybe value;
 val concl = Args.$$$ "concl" -- Args.colon;
 
 val insts =
@@ -387,7 +386,8 @@
 fun method inst_tac tac =
   Args.goal_spec --
   Scan.optional (Scan.lift
-    (P.and_list1 (Args.var -- (Args.$$$ "=" |-- P.!!! Args.name_source)) --| Args.$$$ "in")) [] --
+    (Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.name_source)) --|
+      Args.$$$ "in")) [] --
   Attrib.thms >>
   (fn ((quant, insts), thms) => fn ctxt => METHOD (fn facts =>
     if null insts then quant (Method.insert_tac facts THEN' tac ctxt thms)
@@ -425,5 +425,5 @@
 
 end;
 
-structure BasicRuleInsts: BASIC_RULE_INSTS = RuleInsts;
-open BasicRuleInsts;
+structure Basic_Rule_Insts: BASIC_RULE_INSTS = RuleInsts;
+open Basic_Rule_Insts;
diff -r 080e85d46108 -r 75b8f26f2f07 src/Pure/Isar/spec_parse.ML
--- a/src/Pure/Isar/spec_parse.ML	Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Isar/spec_parse.ML	Sat May 15 23:16:32 2010 +0200
@@ -35,121 +35,129 @@
 structure SpecParse: SPEC_PARSE =
 struct
 
-structure P = OuterParse;
-
-
 (* theorem specifications *)
 
-val attrib = P.position ((P.keyword_ident_or_symbolic || P.xname) -- P.!!! Args.parse) >> Args.src;
-val attribs = P.$$$ "[" |-- P.list attrib --| P.$$$ "]";
+val attrib =
+  Parse.position ((Parse.keyword_ident_or_symbolic || Parse.xname) -- Parse.!!! Args.parse)
+  >> Args.src;
+
+val attribs = Parse.$$$ "[" |-- Parse.list attrib --| Parse.$$$ "]";
 val opt_attribs = Scan.optional attribs [];
 
-fun thm_name s = P.binding -- opt_attribs --| P.$$$ s;
+fun thm_name s = Parse.binding -- opt_attribs --| Parse.$$$ s;
 
 fun opt_thm_name s =
-  Scan.optional ((P.binding -- opt_attribs || attribs >> pair Binding.empty) --| P.$$$ s)
+  Scan.optional ((Parse.binding -- opt_attribs || attribs >> pair Binding.empty) --| Parse.$$$ s)
     Attrib.empty_binding;
 
-val spec = opt_thm_name ":" -- P.prop;
-val specs = opt_thm_name ":" -- Scan.repeat1 P.prop;
+val spec = opt_thm_name ":" -- Parse.prop;
+val specs = opt_thm_name ":" -- Scan.repeat1 Parse.prop;
 
 val alt_specs =
-  P.enum1 "|" (spec --| Scan.option (Scan.ahead (P.name || P.$$$ "[") -- P.!!! (P.$$$ "|")));
+  Parse.enum1 "|"
+    (spec --| Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|")));
 
-val where_alt_specs = P.where_ |-- P.!!! alt_specs;
+val where_alt_specs = Parse.where_ |-- Parse.!!! alt_specs;
 
 val xthm =
-  P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Facts.named "") ||
-  (P.alt_string >> Facts.Fact ||
-    P.position P.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;
+  Parse.$$$ "[" |-- attribs --| Parse.$$$ "]" >> pair (Facts.named "") ||
+  (Parse.alt_string >> Facts.Fact ||
+    Parse.position Parse.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;
 
 val xthms1 = Scan.repeat1 xthm;
 
-val name_facts = P.and_list1 (opt_thm_name "=" -- xthms1);
+val name_facts = Parse.and_list1 (opt_thm_name "=" -- xthms1);
 
 
 (* basic constant specifications *)
 
 val constdecl =
-  P.binding --
-    (P.where_ >> K (NONE, NoSyn) ||
-      P.$$$ "::" |-- P.!!! ((P.typ >> SOME) -- P.opt_mixfix' --| P.where_) ||
-      Scan.ahead (P.$$$ "(") |-- P.!!! (P.mixfix' --| P.where_ >> pair NONE))
-  >> P.triple2;
+  Parse.binding --
+    (Parse.where_ >> K (NONE, NoSyn) ||
+      Parse.$$$ "::" |-- Parse.!!! ((Parse.typ >> SOME) -- Parse.opt_mixfix' --| Parse.where_) ||
+      Scan.ahead (Parse.$$$ "(") |-- Parse.!!! (Parse.mixfix' --| Parse.where_ >> pair NONE))
+  >> Parse.triple2;
 
-val constdef = Scan.option constdecl -- (opt_thm_name ":" -- P.prop);
+val constdef = Scan.option constdecl -- (opt_thm_name ":" -- Parse.prop);
 
 
 (* locale and context elements *)
 
-val locale_mixfix = P.$$$ "(" -- P.$$$ "structure" -- P.!!! (P.$$$ ")") >> K Structure || P.mixfix;
+val locale_mixfix =
+  Parse.$$$ "(" -- Parse.$$$ "structure" -- Parse.!!! (Parse.$$$ ")") >> K Structure ||
+  Parse.mixfix;
 
 val locale_fixes =
-  P.and_list1 (P.binding -- Scan.option (P.$$$ "::" |-- P.typ) -- locale_mixfix
-    >> (single o P.triple1) ||
-  P.params >> map Syntax.no_syn) >> flat;
+  Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- locale_mixfix
+    >> (single o Parse.triple1) ||
+  Parse.params >> map Syntax.no_syn) >> flat;
 
 val locale_insts =
-  Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) []
-  -- Scan.optional (P.where_ |-- P.and_list1 (opt_thm_name ":" -- P.prop)) [];
+  Scan.optional
+    (Parse.$$$ "[" |-- Parse.!!! (Scan.repeat1 (Parse.maybe Parse.term) --| Parse.$$$ "]")) [] --
+  Scan.optional (Parse.where_ |-- Parse.and_list1 (opt_thm_name ":" -- Parse.prop)) [];
 
 local
 
 val loc_element =
-  P.$$$ "fixes" |-- P.!!! locale_fixes >> Element.Fixes ||
-  P.$$$ "constrains" |-- P.!!! (P.and_list1 (P.name -- (P.$$$ "::" |-- P.typ)))
+  Parse.$$$ "fixes" |-- Parse.!!! locale_fixes >> Element.Fixes ||
+  Parse.$$$ "constrains" |--
+    Parse.!!! (Parse.and_list1 (Parse.name -- (Parse.$$$ "::" |-- Parse.typ)))
     >> Element.Constrains ||
-  P.$$$ "assumes" |-- P.!!! (P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp))
+  Parse.$$$ "assumes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp))
     >> Element.Assumes ||
-  P.$$$ "defines" |-- P.!!! (P.and_list1 (opt_thm_name ":" -- P.propp))
+  Parse.$$$ "defines" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Parse.propp))
     >> Element.Defines ||
-  P.$$$ "notes" |-- P.!!! (P.and_list1 (opt_thm_name "=" -- xthms1))
+  Parse.$$$ "notes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name "=" -- xthms1))
     >> (curry Element.Notes "");
 
 fun plus1_unless test scan =
-  scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
+  scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan));
 
 fun prefix mandatory =
-  P.name -- (P.$$$ "!" >> K true || P.$$$ "?" >> K false || Scan.succeed mandatory) --| P.$$$ ":";
+  Parse.name --
+    (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --|
+    Parse.$$$ ":";
 
-val instance = P.where_ |--
-  P.and_list1 (P.name -- (P.$$$ "=" |-- P.term)) >> Expression.Named ||
-  Scan.repeat1 (P.maybe P.term) >> Expression.Positional;
+val instance = Parse.where_ |--
+  Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named ||
+  Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional;
 
 in
 
-val locale_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
-   P.$$$ "defines" || P.$$$ "notes";
+val locale_keyword =
+  Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" ||
+  Parse.$$$ "defines" || Parse.$$$ "notes";
 
-val class_expr = plus1_unless locale_keyword P.xname;
+val class_expr = plus1_unless locale_keyword Parse.xname;
 
 fun locale_expression mandatory =
   let
-    val expr2 = P.xname;
+    val expr2 = Parse.xname;
     val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 --
       Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
     val expr0 = plus1_unless locale_keyword expr1;
-  in expr0 -- Scan.optional (P.$$$ "for" |-- P.!!! locale_fixes) [] end;
+  in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end;
 
-val context_element = P.group "context element" loc_element;
+val context_element = Parse.group "context element" loc_element;
 
 end;
 
 
 (* statements *)
 
-val statement = P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp);
+val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp);
 
 val obtain_case =
-  P.parbinding -- (Scan.optional (P.simple_fixes --| P.where_) [] --
-    (P.and_list1 (Scan.repeat1 P.prop) >> flat));
+  Parse.parbinding -- (Scan.optional (Parse.simple_fixes --| Parse.where_) [] --
+    (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat));
 
 val general_statement =
   statement >> (fn x => ([], Element.Shows x)) ||
   Scan.repeat context_element --
-   (P.$$$ "obtains" |-- P.!!! (P.enum1 "|" obtain_case) >> Element.Obtains ||
-    P.$$$ "shows" |-- P.!!! statement >> Element.Shows);
+   (Parse.$$$ "obtains" |-- Parse.!!! (Parse.enum1 "|" obtain_case) >> Element.Obtains ||
+    Parse.$$$ "shows" |-- Parse.!!! statement >> Element.Shows);
 
-val statement_keyword = P.$$$ "obtains" || P.$$$ "shows";
+val statement_keyword = Parse.$$$ "obtains" || Parse.$$$ "shows";
 
 end;
diff -r 080e85d46108 -r 75b8f26f2f07 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sat May 15 23:16:32 2010 +0200
@@ -660,8 +660,8 @@
   let val st' = command tr st in
     if immediate orelse
       null proof_trs orelse
-      OuterKeyword.is_schematic_goal (name_of tr) orelse
-      exists (OuterKeyword.is_qed_global o name_of) proof_trs orelse
+      Keyword.is_schematic_goal (name_of tr) orelse
+      exists (Keyword.is_qed_global o name_of) proof_trs orelse
       not (can proof_of st') orelse
       Proof.is_relevant (proof_of st')
     then
diff -r 080e85d46108 -r 75b8f26f2f07 src/Pure/Isar/value_parse.ML
--- a/src/Pure/Isar/value_parse.ML	Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Isar/value_parse.ML	Sat May 15 23:16:32 2010 +0200
@@ -19,27 +19,24 @@
 structure ValueParse: VALUE_PARSE =
 struct
 
-structure P = OuterParse;
-
-
 (* syntax utilities *)
 
-fun comma p = P.$$$ "," |-- P.!!! p;
-fun equal p = P.$$$ "=" |-- P.!!! p;
-fun parens p = P.$$$ "(" |-- P.!!! (p --| P.$$$ ")");
+fun comma p = Parse.$$$ "," |-- Parse.!!! p;
+fun equal p = Parse.$$$ "=" |-- Parse.!!! p;
+fun parens p = Parse.$$$ "(" |-- Parse.!!! (p --| Parse.$$$ ")");
 
 
 (* tuples *)
 
 val unit = parens (Scan.succeed ());
 fun pair p1 p2 = parens (p1 -- comma p2);
-fun triple p1 p2 p3 = parens (p1 -- comma p2 -- comma p3) >> P.triple1;
+fun triple p1 p2 p3 = parens (p1 -- comma p2 -- comma p3) >> Parse.triple1;
 
 
 (* lists *)
 
-fun list p = parens (P.enum "," p);
-val properties = list (P.string -- equal P.string);
+fun list p = parens (Parse.enum "," p);
+val properties = list (Parse.string -- equal Parse.string);
 
 end;
 
diff -r 080e85d46108 -r 75b8f26f2f07 src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/ML/ml_antiquote.ML	Sat May 15 23:16:32 2010 +0200
@@ -57,12 +57,11 @@
 
 (** misc antiquotations **)
 
-structure P = OuterParse;
-
 val _ = inline "make_string" (Scan.succeed ml_make_string);
 
 val _ = value "binding"
-  (Scan.lift (P.position Args.name) >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));
+  (Scan.lift (Parse.position Args.name)
+    >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));
 
 val _ = value "theory"
   (Scan.lift Args.name >> (fn name => "ThyInfo.get_theory " ^ ML_Syntax.print_string name)
@@ -80,11 +79,12 @@
 val _ = inline "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term));
 
 val _ = macro "let" (Args.context --
-  Scan.lift (P.and_list1 (P.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source)))
+  Scan.lift
+    (Parse.and_list1 (Parse.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source)))
     >> (fn (ctxt, args) => #2 (ProofContext.match_bind true args ctxt)));
 
 val _ = macro "note" (Args.context :|-- (fn ctxt =>
-  P.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) =>
+  Parse.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) =>
     ((a, map (Attrib.attribute (ProofContext.theory_of ctxt)) srcs), [(ths, [])])))
   >> (fn args => #2 (ProofContext.note_thmss "" args ctxt))));
 
@@ -118,7 +118,7 @@
 
 (* type constructors *)
 
-fun type_name kind check = Args.context -- Scan.lift (OuterParse.position Args.name_source)
+fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_source)
   >> (fn (ctxt, (s, pos)) =>
     let
       val Type (c, _) = ProofContext.read_type_name_proper ctxt false s;
@@ -137,7 +137,7 @@
 
 (* constants *)
 
-fun const_name check = Args.context -- Scan.lift (OuterParse.position Args.name_source)
+fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_source)
   >> (fn (ctxt, (s, pos)) =>
     let
       val Const (c, _) = ProofContext.read_const_proper ctxt false s;
@@ -151,13 +151,13 @@
 
 
 val _ = inline "syntax_const"
-  (Args.context -- Scan.lift (OuterParse.position Args.name) >> (fn (ctxt, (c, pos)) =>
+  (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) =>
     if Syntax.is_const (ProofContext.syn_of ctxt) c then ML_Syntax.print_string c
     else error ("Unknown syntax const: " ^ quote c ^ Position.str_of pos)));
 
 val _ = inline "const"
   (Args.context -- Scan.lift Args.name_source -- Scan.optional
-      (Scan.lift (Args.$$$ "(") |-- OuterParse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
+      (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
     >> (fn ((ctxt, raw_c), Ts) =>
       let
         val Const (c, _) = ProofContext.read_const_proper ctxt true raw_c;
diff -r 080e85d46108 -r 75b8f26f2f07 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/ML/ml_context.ML	Sat May 15 23:16:32 2010 +0200
@@ -112,11 +112,10 @@
 
 local
 
-structure P = OuterParse;
 structure T = OuterLex;
 
 val antiq =
-  P.!!! (P.position P.xname -- Args.parse --| Scan.ahead P.eof)
+  Parse.!!! (Parse.position Parse.xname -- Args.parse --| Scan.ahead Parse.eof)
   >> (fn ((x, pos), y) => Args.src ((x, y), pos));
 
 val begin_env = ML_Lex.tokenize "structure Isabelle =\nstruct\n";
@@ -138,7 +137,7 @@
               NONE => error ("No context -- cannot expand ML antiquotations" ^ Position.str_of pos)
             | SOME ctxt => Context.proof_of ctxt);
 
-          val lex = #1 (OuterKeyword.get_lexicons ());
+          val lex = #1 (Keyword.get_lexicons ());
           fun no_decl _ = ([], []);
 
           fun expand (Antiquote.Text tok) state = (K ([], [tok]), state)
diff -r 080e85d46108 -r 75b8f26f2f07 src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/ML/ml_thms.ML	Sat May 15 23:16:32 2010 +0200
@@ -54,7 +54,7 @@
 
 val _ = ML_Context.add_antiq "lemma"
   (fn _ => Args.context -- Args.mode "open" --
-      Scan.lift (OuterParse.and_list1 (Scan.repeat1 goal) --
+      Scan.lift (Parse.and_list1 (Scan.repeat1 goal) --
         (by |-- Method.parse -- Scan.option Method.parse)) >>
     (fn ((ctxt, is_open), (raw_propss, methods)) => fn background =>
       let
diff -r 080e85d46108 -r 75b8f26f2f07 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Proof/extraction.ML	Sat May 15 23:16:32 2010 +0200
@@ -750,31 +750,29 @@
 
 (**** interface ****)
 
-structure P = OuterParse and K = OuterKeyword;
-
-val parse_vars = Scan.optional (P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") [];
+val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") [];
 
 val _ =
   OuterSyntax.command "realizers"
   "specify realizers for primitive axioms / theorems, together with correctness proof"
-  K.thy_decl
-    (Scan.repeat1 (P.xname -- parse_vars --| P.$$$ ":" -- P.string -- P.string) >>
+  Keyword.thy_decl
+    (Scan.repeat1 (Parse.xname -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
      (fn xs => Toplevel.theory (fn thy => add_realizers
        (map (fn (((a, vs), s1), s2) => (PureThy.get_thm thy a, (vs, s1, s2))) xs) thy)));
 
 val _ =
   OuterSyntax.command "realizability"
-  "add equations characterizing realizability" K.thy_decl
-  (Scan.repeat1 P.string >> (Toplevel.theory o add_realizes_eqns));
+  "add equations characterizing realizability" Keyword.thy_decl
+  (Scan.repeat1 Parse.string >> (Toplevel.theory o add_realizes_eqns));
 
 val _ =
   OuterSyntax.command "extract_type"
-  "add equations characterizing type of extracted program" K.thy_decl
-  (Scan.repeat1 P.string >> (Toplevel.theory o add_typeof_eqns));
+  "add equations characterizing type of extracted program" Keyword.thy_decl
+  (Scan.repeat1 Parse.string >> (Toplevel.theory o add_typeof_eqns));
 
 val _ =
-  OuterSyntax.command "extract" "extract terms from proofs" K.thy_decl
-    (Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
+  OuterSyntax.command "extract" "extract terms from proofs" Keyword.thy_decl
+    (Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
       extract (map (apfst (PureThy.get_thm thy)) xs) thy)));
 
 val etype_of = etype_of o add_syntax;
diff -r 080e85d46108 -r 75b8f26f2f07 src/Pure/ProofGeneral/pgip_parser.ML
--- a/src/Pure/ProofGeneral/pgip_parser.ML	Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/ProofGeneral/pgip_parser.ML	Sat May 15 23:16:32 2010 +0200
@@ -12,7 +12,6 @@
 structure PgipParser: PGIP_PARSER =
 struct
 
-structure K = OuterKeyword;
 structure D = PgipMarkup;
 structure I = PgipIsabelle;
 
@@ -51,42 +50,42 @@
 fun closegoal text = [D.Closegoal {text = text}, D.Closeblock {}];
 
 
-fun command k f = Symtab.update_new (OuterKeyword.kind_of k, f);
+fun command k f = Symtab.update_new (Keyword.kind_of k, f);
 
 val command_keywords = Symtab.empty
-  |> command K.control          badcmd
-  |> command K.diag             (fn text => [D.Spuriouscmd {text = text}])
-  |> command K.thy_begin        thy_begin
-  |> command K.thy_switch       badcmd
-  |> command K.thy_end          (fn text => [D.Closeblock {}, D.Closetheory {text = text}])
-  |> command K.thy_heading      thy_heading
-  |> command K.thy_decl         thy_decl
-  |> command K.thy_script       thy_decl
-  |> command K.thy_goal         goal
-  |> command K.thy_schematic_goal goal
-  |> command K.qed              closegoal
-  |> command K.qed_block        closegoal
-  |> command K.qed_global       (fn text => [D.Giveupgoal {text = text}])
-  |> command K.prf_heading      (fn text => [D.Doccomment {text = text}])
-  |> command K.prf_goal         goal
-  |> command K.prf_block        prf_block
-  |> command K.prf_open         prf_open
-  |> command K.prf_close        (fn text => [D.Proofstep {text = text}, D.Closeblock {}])
-  |> command K.prf_chain        proofstep
-  |> command K.prf_decl         proofstep
-  |> command K.prf_asm          proofstep
-  |> command K.prf_asm_goal     goal
-  |> command K.prf_script       proofstep;
+  |> command Keyword.control          badcmd
+  |> command Keyword.diag             (fn text => [D.Spuriouscmd {text = text}])
+  |> command Keyword.thy_begin        thy_begin
+  |> command Keyword.thy_switch       badcmd
+  |> command Keyword.thy_end          (fn text => [D.Closeblock {}, D.Closetheory {text = text}])
+  |> command Keyword.thy_heading      thy_heading
+  |> command Keyword.thy_decl         thy_decl
+  |> command Keyword.thy_script       thy_decl
+  |> command Keyword.thy_goal         goal
+  |> command Keyword.thy_schematic_goal goal
+  |> command Keyword.qed              closegoal
+  |> command Keyword.qed_block        closegoal
+  |> command Keyword.qed_global       (fn text => [D.Giveupgoal {text = text}])
+  |> command Keyword.prf_heading      (fn text => [D.Doccomment {text = text}])
+  |> command Keyword.prf_goal         goal
+  |> command Keyword.prf_block        prf_block
+  |> command Keyword.prf_open         prf_open
+  |> command Keyword.prf_close        (fn text => [D.Proofstep {text = text}, D.Closeblock {}])
+  |> command Keyword.prf_chain        proofstep
+  |> command Keyword.prf_decl         proofstep
+  |> command Keyword.prf_asm          proofstep
+  |> command Keyword.prf_asm_goal     goal
+  |> command Keyword.prf_script       proofstep;
 
-val _ = subset (op =) (OuterKeyword.kinds, Symtab.keys command_keywords)
+val _ = subset (op =) (Keyword.kinds, Symtab.keys command_keywords)
   orelse sys_error "Incomplete coverage of command keywords";
 
 fun parse_command "sorry" text = [D.Postponegoal {text = text}, D.Closeblock {}]
   | parse_command name text =
-      (case OuterKeyword.command_keyword name of
+      (case Keyword.command_keyword name of
         NONE => [D.Unparseable {text = text}]
       | SOME k =>
-          (case Symtab.lookup command_keywords (OuterKeyword.kind_of k) of
+          (case Symtab.lookup command_keywords (Keyword.kind_of k) of
             NONE => [D.Unparseable {text = text}]
           | SOME f => f text));
 
@@ -104,6 +103,6 @@
 
 
 fun pgip_parser pos str =
-  maps parse_span (ThySyntax.parse_spans (OuterKeyword.get_lexicons ()) pos str);
+  maps parse_span (ThySyntax.parse_spans (Keyword.get_lexicons ()) pos str);
 
 end;
diff -r 080e85d46108 -r 75b8f26f2f07 src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat May 15 23:16:32 2010 +0200
@@ -188,48 +188,44 @@
 
 (* additional outer syntax for Isar *)
 
-local structure P = OuterParse and K = OuterKeyword in
-
 fun prP () =
-  OuterSyntax.improper_command "ProofGeneral.pr" "print state (internal)" K.diag
+  OuterSyntax.improper_command "ProofGeneral.pr" "print state (internal)" Keyword.diag
     (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
       if Toplevel.is_toplevel state orelse Toplevel.is_theory state then tell_clear_goals ()
       else (Toplevel.quiet := false; Toplevel.print_state true state))));
 
 fun undoP () = (*undo without output -- historical*)
-  OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
+  OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" Keyword.control
     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1)));
 
 fun restartP () =
-  OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
-    (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
+  OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" Keyword.control
+    (Parse.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
 
 fun kill_proofP () =
-  OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
+  OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" Keyword.control
     (Scan.succeed (Toplevel.no_timing o
       Toplevel.imperative (fn () => (Isar.kill_proof (); tell_clear_goals ()))));
 
 fun inform_file_processedP () =
-  OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
-    (P.name >> (fn file =>
+  OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" Keyword.control
+    (Parse.name >> (fn file =>
       Toplevel.no_timing o Toplevel.imperative (fn () => inform_file_processed file)));
 
 fun inform_file_retractedP () =
-  OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
-    (P.name >> (Toplevel.no_timing oo
+  OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" Keyword.control
+    (Parse.name >> (Toplevel.no_timing oo
       (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
 
 fun process_pgipP () =
-  OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
-    (P.text >> (Toplevel.no_timing oo
+  OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" Keyword.control
+    (Parse.text >> (Toplevel.no_timing oo
       (fn txt => Toplevel.imperative (fn () => ProofGeneralPgip.process_pgip txt))));
 
 fun init_outer_syntax () = List.app (fn f => f ())
   [prP, undoP, restartP, kill_proofP, inform_file_processedP,
     inform_file_retractedP, process_pgipP];
 
-end;
-
 
 (* init *)
 
diff -r 080e85d46108 -r 75b8f26f2f07 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat May 15 23:16:32 2010 +0200
@@ -312,8 +312,8 @@
 (** lexicalstructure element with keywords (PGIP version of elisp keywords file) **)
 
 fun lexicalstructure_keywords () =
-    let val keywords = OuterKeyword.dest_keywords ()
-        val commands = OuterKeyword.dest_commands ()
+    let val keywords = Keyword.dest_keywords ()
+        val commands = Keyword.dest_commands ()
         fun keyword_elt kind keyword =
             XML.Elem("keyword", [("word", keyword), ("category", kind)], [])
         in
@@ -1013,8 +1013,8 @@
 (* Extra command for embedding prover-control inside document (obscure/debug usage). *)
 
 fun init_outer_syntax () =
-  OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" OuterKeyword.control
-    (OuterParse.text >> (Toplevel.no_timing oo
+  OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" Keyword.control
+    (Parse.text >> (Toplevel.no_timing oo
       (fn txt => Toplevel.imperative (fn () => process_pgip_plain txt))));
 
 
diff -r 080e85d46108 -r 75b8f26f2f07 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML	Sat May 15 23:16:32 2010 +0200
@@ -89,9 +89,9 @@
 
 fun init out =
  (Unsynchronized.change print_mode
-    (fold (update op =) [isabelle_processN, OuterKeyword.keyword_status_reportN, Pretty.symbolicN]);
+    (fold (update op =) [isabelle_processN, Keyword.keyword_status_reportN, Pretty.symbolicN]);
   setup_channels out |> init_message;
-  OuterKeyword.report ();
+  Keyword.report ();
   Output.status (Markup.markup Markup.ready "");
   Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
 
diff -r 080e85d46108 -r 75b8f26f2f07 src/Pure/System/isar.ML
--- a/src/Pure/System/isar.ML	Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/System/isar.ML	Sat May 15 23:16:32 2010 +0200
@@ -80,14 +80,14 @@
 fun linear_undo n = edit_history n (K (find_and_undo (K true)));
 
 fun undo n = edit_history n (fn st => fn hist =>
-  find_and_undo (if Toplevel.is_proof st then K true else OuterKeyword.is_theory) hist);
+  find_and_undo (if Toplevel.is_proof st then K true else Keyword.is_theory) hist);
 
 fun kill () = edit_history 1 (fn st => fn hist =>
   find_and_undo
-    (if Toplevel.is_proof st then OuterKeyword.is_theory else OuterKeyword.is_theory_begin) hist);
+    (if Toplevel.is_proof st then Keyword.is_theory else Keyword.is_theory_begin) hist);
 
 fun kill_proof () = edit_history 1 (fn st => fn hist =>
-  if Toplevel.is_proof st then find_and_undo OuterKeyword.is_theory hist
+  if Toplevel.is_proof st then find_and_undo Keyword.is_theory hist
   else raise Toplevel.UNDEF);
 
 end;
@@ -102,9 +102,9 @@
   | SOME (st', NONE) =>
       let
         val name = Toplevel.name_of tr;
-        val _ = if OuterKeyword.is_theory_begin name then init () else ();
+        val _ = if Keyword.is_theory_begin name then init () else ();
         val _ =
-          if OuterKeyword.is_regular name
+          if Keyword.is_regular name
           then edit_history 1 (fn st => fn hist => (st', (st, tr) :: hist)) else ();
       in true end);
 
@@ -157,7 +157,6 @@
 
 local
 
-structure P = OuterParse and K = OuterKeyword;
 val op >> = Scan.>>;
 
 in
@@ -165,33 +164,35 @@
 (* global history *)
 
 val _ =
-  OuterSyntax.improper_command "init_toplevel" "init toplevel point-of-interest" K.control
+  OuterSyntax.improper_command "init_toplevel" "init toplevel point-of-interest" Keyword.control
     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative init));
 
 val _ =
-  OuterSyntax.improper_command "linear_undo" "undo commands" K.control
-    (Scan.optional P.nat 1 >>
+  OuterSyntax.improper_command "linear_undo" "undo commands" Keyword.control
+    (Scan.optional Parse.nat 1 >>
       (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => linear_undo n)));
 
 val _ =
-  OuterSyntax.improper_command "undo" "undo commands (skipping closed proofs)" K.control
-    (Scan.optional P.nat 1 >>
+  OuterSyntax.improper_command "undo" "undo commands (skipping closed proofs)" Keyword.control
+    (Scan.optional Parse.nat 1 >>
       (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => undo n)));
 
 val _ =
-  OuterSyntax.improper_command "undos_proof" "undo commands (skipping closed proofs)" K.control
-    (Scan.optional P.nat 1 >> (fn n => Toplevel.no_timing o
+  OuterSyntax.improper_command "undos_proof" "undo commands (skipping closed proofs)"
+    Keyword.control
+    (Scan.optional Parse.nat 1 >> (fn n => Toplevel.no_timing o
       Toplevel.keep (fn state =>
         if Toplevel.is_proof state then (undo n; print ()) else raise Toplevel.UNDEF)));
 
 val _ =
-  OuterSyntax.improper_command "cannot_undo" "partial undo -- Proof General legacy" K.control
-    (P.name >>
+  OuterSyntax.improper_command "cannot_undo" "partial undo -- Proof General legacy"
+    Keyword.control
+    (Parse.name >>
       (fn "end" => Toplevel.no_timing o Toplevel.imperative (fn () => undo 1)
         | txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt))));
 
 val _ =
-  OuterSyntax.improper_command "kill" "kill partial proof or theory development" K.control
+  OuterSyntax.improper_command "kill" "kill partial proof or theory development" Keyword.control
     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
 
 end;
diff -r 080e85d46108 -r 75b8f26f2f07 src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/System/session.ML	Sat May 15 23:16:32 2010 +0200
@@ -48,7 +48,7 @@
     (if Distribution.changelog <> "" then "\nSee also " ^ Distribution.changelog else "");
 
 val _ =
-  OuterSyntax.improper_command "welcome" "print welcome message" OuterKeyword.diag
+  OuterSyntax.improper_command "welcome" "print welcome message" Keyword.diag
     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (writeln o welcome)));
 
 
diff -r 080e85d46108 -r 75b8f26f2f07 src/Pure/Thy/term_style.ML
--- a/src/Pure/Thy/term_style.ML	Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Thy/term_style.ML	Sat May 15 23:16:32 2010 +0200
@@ -43,7 +43,7 @@
 
 (* style parsing *)
 
-fun parse_single ctxt = OuterParse.position (OuterParse.xname -- Args.parse)
+fun parse_single ctxt = Parse.position (Parse.xname -- Args.parse)
   >> (fn x as ((name, _), _) => fst (Args.context_syntax "style"
        (Scan.lift (the_style (ProofContext.theory_of ctxt) name))
          (Args.src x) ctxt |>> (fn f => f ctxt)));
diff -r 080e85d46108 -r 75b8f26f2f07 src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Thy/thy_header.ML	Sat May 15 23:16:32 2010 +0200
@@ -15,7 +15,6 @@
 struct
 
 structure T = OuterLex;
-structure P = OuterParse;
 
 
 (* keywords *)
@@ -32,23 +31,28 @@
 
 (* header args *)
 
-val file_name = P.group "file name" P.name;
-val theory_name = P.group "theory name" P.name;
+val file_name = Parse.group "file name" Parse.name;
+val theory_name = Parse.group "theory name" Parse.name;
 
-val file = P.$$$ "(" |-- P.!!! (file_name --| P.$$$ ")") >> rpair false || file_name >> rpair true;
-val uses = Scan.optional (P.$$$ usesN |-- P.!!! (Scan.repeat1 file)) [];
+val file =
+  Parse.$$$ "(" |-- Parse.!!! (file_name --| Parse.$$$ ")") >> rpair false ||
+  file_name >> rpair true;
+
+val uses = Scan.optional (Parse.$$$ usesN |-- Parse.!!! (Scan.repeat1 file)) [];
 
 val args =
-  theory_name -- (P.$$$ importsN |-- P.!!! (Scan.repeat1 theory_name -- uses --| P.$$$ beginN))
-  >> P.triple2;
+  theory_name -- (Parse.$$$ importsN |--
+    Parse.!!! (Scan.repeat1 theory_name -- uses --| Parse.$$$ beginN))
+  >> Parse.triple2;
 
 
 (* read header *)
 
 val header =
-  (P.$$$ headerN -- P.tags) |-- (P.!!! (P.doc_source -- Scan.repeat P.semicolon --
-    (P.$$$ theoryN -- P.tags) |-- args)) ||
-  (P.$$$ theoryN -- P.tags) |-- P.!!! args;
+  (Parse.$$$ headerN -- Parse.tags) |--
+    (Parse.!!! (Parse.doc_source -- Scan.repeat Parse.semicolon --
+      (Parse.$$$ theoryN -- Parse.tags) |-- args)) ||
+  (Parse.$$$ theoryN -- Parse.tags) |-- Parse.!!! args;
 
 fun read pos src =
   let val res =
@@ -56,7 +60,7 @@
     |> Symbol.source {do_recover = false}
     |> T.source {do_recover = NONE} (fn () => (header_lexicon, Scan.empty_lexicon)) pos
     |> T.source_proper
-    |> Source.source T.stopper (Scan.single (Scan.error (P.!!! header))) NONE
+    |> Source.source T.stopper (Scan.single (Scan.error (Parse.!!! header))) NONE
     |> Source.get_single;
   in
     (case res of SOME (x, _) => x
diff -r 080e85d46108 -r 75b8f26f2f07 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML	Sat May 15 23:16:32 2010 +0200
@@ -37,7 +37,6 @@
 struct
 
 structure T = OuterLex;
-structure P = OuterParse;
 
 
 (** global options **)
@@ -132,12 +131,16 @@
 
 local
 
-val property = P.xname -- Scan.optional (P.$$$ "=" |-- P.!!! P.xname) "";
-val properties = Scan.optional (P.$$$ "[" |-- P.!!! (P.enum "," property --| P.$$$ "]")) [];
+val property =
+  Parse.xname -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.xname) "";
+
+val properties =
+  Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.enum "," property --| Parse.$$$ "]")) [];
 
 in
 
-val antiq = P.!!! (P.position P.xname -- properties -- Args.parse --| Scan.ahead P.eof)
+val antiq =
+  Parse.!!! (Parse.position Parse.xname -- properties -- Args.parse --| Scan.ahead Parse.eof)
   >> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos)));
 
 end;
@@ -249,7 +252,7 @@
     val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span;
 
     val (tag, tags) = tag_stack;
-    val tag' = try hd (fold OuterKeyword.update_tags cmd_tags (the_list tag));
+    val tag' = try hd (fold Keyword.update_tags cmd_tags (the_list tag));
 
     val active_tag' =
       if is_some tag' then tag'
@@ -316,11 +319,11 @@
     (if d = 0 then Scan.fail_with (K "Bad nesting of meta-comments") else opt_newline)
     >> pair (d - 1));
 
-val tag = (improper -- P.$$$ "%" -- improper) |-- P.!!! (P.tag_name --| blank_end);
+val tag = (improper -- Parse.$$$ "%" -- improper) |-- Parse.!!! (Parse.tag_name --| blank_end);
 
 val locale =
-  Scan.option ((P.$$$ "(" -- improper -- P.$$$ "in") |--
-    P.!!! (improper |-- P.xname --| (improper -- P.$$$ ")")));
+  Scan.option ((Parse.$$$ "(" -- improper -- Parse.$$$ "in") |--
+    Parse.!!! (improper |-- Parse.xname --| (improper -- Parse.$$$ ")")));
 
 in
 
@@ -332,26 +335,27 @@
       >> (fn d => (NONE, (NoToken, ("", d))));
 
     fun markup mark mk flag = Scan.peek (fn d =>
-      improper |-- P.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.content_of)) --
+      improper |--
+        Parse.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.content_of)) --
       Scan.repeat tag --
-      P.!!!! ((improper -- locale -- improper) |-- P.doc_source --| improper_end)
+      Parse.!!!! ((improper -- locale -- improper) |-- Parse.doc_source --| improper_end)
       >> (fn (((tok, pos), tags), txt) =>
         let val name = T.content_of tok
         in (SOME (name, pos, tags), (mk (name, txt), (flag, d))) end));
 
     val command = Scan.peek (fn d =>
-      P.position (Scan.one (T.is_kind T.Command)) --
+      Parse.position (Scan.one (T.is_kind T.Command)) --
       Scan.repeat tag
       >> (fn ((tok, pos), tags) =>
         let val name = T.content_of tok
         in (SOME (name, pos, tags), (BasicToken tok, (Latex.markup_false, d))) end));
 
     val cmt = Scan.peek (fn d =>
-      P.$$$ "--" |-- P.!!!! (improper |-- P.doc_source)
+      Parse.$$$ "--" |-- Parse.!!!! (improper |-- Parse.doc_source)
       >> (fn txt => (NONE, (MarkupToken ("cmt", txt), ("", d)))));
 
     val other = Scan.peek (fn d =>
-       P.not_eof >> (fn tok => (NONE, (BasicToken tok, ("", d)))));
+       Parse.not_eof >> (fn tok => (NONE, (BasicToken tok, ("", d)))));
 
     val token =
       ignored ||
@@ -565,7 +569,7 @@
 
 (* embedded lemma *)
 
-val _ = OuterKeyword.keyword "by";
+val _ = Keyword.keyword "by";
 
 val _ = antiquotation "lemma"
   (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse))
diff -r 080e85d46108 -r 75b8f26f2f07 src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.ML	Sat May 15 23:16:32 2010 +0200
@@ -29,9 +29,7 @@
 structure ThySyntax: THY_SYNTAX =
 struct
 
-structure K = OuterKeyword;
 structure T = OuterLex;
-structure P = OuterParse;
 
 
 (** tokens **)
@@ -111,10 +109,11 @@
 
 val is_whitespace = T.is_kind T.Space orf T.is_kind T.Comment;
 
-val body = Scan.unless (Scan.many is_whitespace -- Scan.ahead (P.command || P.eof)) P.not_eof;
+val body =
+  Scan.unless (Scan.many is_whitespace -- Scan.ahead (Parse.command || Parse.eof)) Parse.not_eof;
 
 val span =
-  Scan.ahead P.command -- P.not_eof -- Scan.repeat body
+  Scan.ahead Parse.command -- Parse.not_eof -- Scan.repeat body
     >> (fn ((name, c), bs) => Span (Command name, c :: bs)) ||
   Scan.many1 is_whitespace >> (fn toks => Span (Ignored, toks)) ||
   Scan.repeat1 body >> (fn toks => Span (Malformed, toks));
@@ -175,13 +174,13 @@
 val proof = Scan.pass 1 (Scan.repeat (Scan.depend (fn d =>
   if d <= 0 then Scan.fail
   else
-    command_with K.is_qed_global >> pair ~1 ||
-    command_with K.is_proof_goal >> pair (d + 1) ||
-    (if d = 0 then Scan.fail else command_with K.is_qed >> pair (d - 1)) ||
-    Scan.unless (command_with K.is_theory) (Scan.one not_eof) >> pair d)) -- Scan.state);
+    command_with Keyword.is_qed_global >> pair ~1 ||
+    command_with Keyword.is_proof_goal >> pair (d + 1) ||
+    (if d = 0 then Scan.fail else command_with Keyword.is_qed >> pair (d - 1)) ||
+    Scan.unless (command_with Keyword.is_theory) (Scan.one not_eof) >> pair d)) -- Scan.state);
 
 val unit =
-  command_with K.is_theory_goal -- proof >> (fn (a, (bs, d)) => (a, bs, d >= 0)) ||
+  command_with Keyword.is_theory_goal -- proof >> (fn (a, (bs, d)) => (a, bs, d >= 0)) ||
   Scan.one not_eof >> (fn a => (a, [], true));
 
 in
diff -r 080e85d46108 -r 75b8f26f2f07 src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Tools/find_consts.ML	Sat May 15 23:16:32 2010 +0200
@@ -148,23 +148,15 @@
   Toplevel.unknown_theory o Toplevel.keep (fn state =>
     find_consts (Proof.context_of (Toplevel.enter_proof_body state)) spec);
 
-local
-
-structure P = OuterParse and K = OuterKeyword;
-
 val criterion =
-  P.reserved "strict" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Strict ||
-  P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Name ||
-  P.xname >> Loose;
-
-in
+  Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Strict ||
+  Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
+  Parse.xname >> Loose;
 
 val _ =
-  OuterSyntax.improper_command "find_consts" "search constants by type pattern" K.diag
-    (Scan.repeat ((Scan.option P.minus >> is_none) -- criterion)
+  OuterSyntax.improper_command "find_consts" "search constants by type pattern" Keyword.diag
+    (Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion)
       >> (Toplevel.no_timing oo find_consts_cmd));
 
 end;
 
-end;
-
diff -r 080e85d46108 -r 75b8f26f2f07 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Sat May 15 23:16:32 2010 +0200
@@ -465,28 +465,27 @@
 
 local
 
-structure P = OuterParse and K = OuterKeyword;
-
 val criterion =
-  P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Name ||
-  P.reserved "intro" >> K Intro ||
-  P.reserved "introiff" >> K IntroIff ||
-  P.reserved "elim" >> K Elim ||
-  P.reserved "dest" >> K Dest ||
-  P.reserved "solves" >> K Solves ||
-  P.reserved "simp" |-- P.!!! (P.$$$ ":" |-- P.term) >> Simp ||
-  P.term >> Pattern;
+  Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
+  Parse.reserved "intro" >> K Intro ||
+  Parse.reserved "introiff" >> K IntroIff ||
+  Parse.reserved "elim" >> K Elim ||
+  Parse.reserved "dest" >> K Dest ||
+  Parse.reserved "solves" >> K Solves ||
+  Parse.reserved "simp" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.term) >> Simp ||
+  Parse.term >> Pattern;
 
 val options =
   Scan.optional
-    (P.$$$ "(" |--
-      P.!!! (Scan.option P.nat -- Scan.optional (P.reserved "with_dups" >> K false) true
-        --| P.$$$ ")")) (NONE, true);
+    (Parse.$$$ "(" |--
+      Parse.!!! (Scan.option Parse.nat -- Scan.optional (Parse.reserved "with_dups" >> K false) true
+        --| Parse.$$$ ")")) (NONE, true);
 in
 
 val _ =
-  OuterSyntax.improper_command "find_theorems" "print theorems meeting specified criteria" K.diag
-    (options -- Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
+  OuterSyntax.improper_command "find_theorems" "print theorems meeting specified criteria"
+    Keyword.diag
+    (options -- Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion))
       >> (Toplevel.no_timing oo find_theorems_cmd));
 
 end;
diff -r 080e85d46108 -r 75b8f26f2f07 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/codegen.ML	Sat May 15 23:16:32 2010 +0200
@@ -959,44 +959,42 @@
    | _ => error ("Malformed annotation: " ^ quote s));
 
 
-structure P = OuterParse and K = OuterKeyword;
-
-val _ = List.app OuterKeyword.keyword ["attach", "file", "contains"];
+val _ = List.app Keyword.keyword ["attach", "file", "contains"];
 
 fun strip_whitespace s = implode (fst (take_suffix (fn c => c = "\n" orelse c = " ")
   (snd (take_prefix (fn c => c = "\n" orelse c = " ") (explode s))))) ^ "\n";
 
-val parse_attach = Scan.repeat (P.$$$ "attach" |--
-  Scan.optional (P.$$$ "(" |-- P.xname --| P.$$$ ")") "" --
-    (P.verbatim >> strip_whitespace));
+val parse_attach = Scan.repeat (Parse.$$$ "attach" |--
+  Scan.optional (Parse.$$$ "(" |-- Parse.xname --| Parse.$$$ ")") "" --
+    (Parse.verbatim >> strip_whitespace));
 
 val _ =
   OuterSyntax.command "types_code"
-  "associate types with target language types" K.thy_decl
-    (Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
+  "associate types with target language types" Keyword.thy_decl
+    (Scan.repeat1 (Parse.xname --| Parse.$$$ "(" -- Parse.string --| Parse.$$$ ")" -- parse_attach) >>
      (fn xs => Toplevel.theory (fn thy => fold (assoc_type o
        (fn ((name, mfx), aux) => (name, (parse_mixfix
          (Syntax.read_typ_global thy) mfx, aux)))) xs thy)));
 
 val _ =
   OuterSyntax.command "consts_code"
-  "associate constants with target language code" K.thy_decl
+  "associate constants with target language code" Keyword.thy_decl
     (Scan.repeat1
-       (P.term --|
-        P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
+       (Parse.term --|
+        Parse.$$$ "(" -- Parse.string --| Parse.$$$ ")" -- parse_attach) >>
      (fn xs => Toplevel.theory (fn thy => fold (assoc_const o
        (fn ((const, mfx), aux) =>
          (const, (parse_mixfix (Syntax.read_term_global thy) mfx, aux)))) xs thy)));
 
 fun parse_code lib =
-  Scan.optional (P.$$$ "(" |-- P.enum "," P.xname --| P.$$$ ")") (!mode) --
-  (if lib then Scan.optional P.name "" else P.name) --
-  Scan.option (P.$$$ "file" |-- P.name) --
+  Scan.optional (Parse.$$$ "(" |-- Parse.enum "," Parse.xname --| Parse.$$$ ")") (!mode) --
+  (if lib then Scan.optional Parse.name "" else Parse.name) --
+  Scan.option (Parse.$$$ "file" |-- Parse.name) --
   (if lib then Scan.succeed []
-   else Scan.optional (P.$$$ "imports" |-- Scan.repeat1 P.name) []) --|
-  P.$$$ "contains" --
-  (   Scan.repeat1 (P.name --| P.$$$ "=" -- P.term)
-   || Scan.repeat1 (P.term >> pair "")) >>
+   else Scan.optional (Parse.$$$ "imports" |-- Scan.repeat1 Parse.name) []) --|
+  Parse.$$$ "contains" --
+  (   Scan.repeat1 (Parse.name --| Parse.$$$ "=" -- Parse.term)
+   || Scan.repeat1 (Parse.term >> pair "")) >>
   (fn ((((mode', module), opt_fname), modules), xs) => Toplevel.theory (fn thy =>
     let
       val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode');
@@ -1021,12 +1019,12 @@
 
 val _ =
   OuterSyntax.command "code_library"
-    "generates code for terms (one structure for each theory)" K.thy_decl
+    "generates code for terms (one structure for each theory)" Keyword.thy_decl
     (parse_code true);
 
 val _ =
   OuterSyntax.command "code_module"
-    "generates code for terms (single structure, incremental)" K.thy_decl
+    "generates code for terms (single structure, incremental)" Keyword.thy_decl
     (parse_code false);
 
 end;