# HG changeset patch
# User wenzelm
# Date 1274133255 -7200
# Node ID 01594f816e3a6dbc92a7f3ca80444d7d12d46dfc
# Parent  f5417836dbead656bee2e399b8b87902bb9d1cdb
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
eliminated old-style structure aliases K = Keyword, P = Parse;

diff -r f5417836dbea -r 01594f816e3a src/FOL/ex/Iff_Oracle.thy
--- a/src/FOL/ex/Iff_Oracle.thy	Mon May 17 15:11:25 2010 +0200
+++ b/src/FOL/ex/Iff_Oracle.thy	Mon May 17 23:54:15 2010 +0200
@@ -52,7 +52,7 @@
 subsection {* Oracle as proof method *}
 
 method_setup iff = {*
-  Scan.lift OuterParse.nat >> (fn n => fn ctxt =>
+  Scan.lift Parse.nat >> (fn n => fn ctxt =>
     SIMPLE_METHOD
       (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt, n)))
         handle Fail _ => no_tac))
diff -r f5417836dbea -r 01594f816e3a src/HOL/Boogie/Tools/boogie_commands.ML
--- a/src/HOL/Boogie/Tools/boogie_commands.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Mon May 17 23:54:15 2010 +0200
@@ -263,31 +263,31 @@
 fun scan_arg f = Args.parens f
 fun scan_opt n = Scan.optional (scan_arg (Args.$$$ n >> K true)) false
 
-val vc_offsets = Scan.optional (Args.bracks (OuterParse.list1
-  (OuterParse.string --| Args.colon -- OuterParse.nat))) []
+val vc_offsets = Scan.optional (Args.bracks (Parse.list1
+  (Parse.string --| Args.colon -- Parse.nat))) []
 
 val _ =
-  OuterSyntax.command "boogie_open"
+  Outer_Syntax.command "boogie_open"
     "Open a new Boogie environment and load a Boogie-generated .b2i file."
-    OuterKeyword.thy_decl
-    (scan_opt "quiet" -- OuterParse.name -- vc_offsets >> 
+    Keyword.thy_decl
+    (scan_opt "quiet" -- Parse.name -- vc_offsets >> 
       (Toplevel.theory o boogie_open))
 
 
-val vc_name = OuterParse.name
+val vc_name = Parse.name
 
-val vc_label = OuterParse.name
+val vc_label = Parse.name
 val vc_labels = Scan.repeat1 vc_label
 
 val vc_paths =
-  OuterParse.nat -- (Args.$$$ "-" |-- OuterParse.nat) >> (op upto) ||
-  OuterParse.nat >> single
+  Parse.nat -- (Args.$$$ "-" |-- Parse.nat) >> (op upto) ||
+  Parse.nat >> single
 
 val vc_opts =
   scan_arg
    (scan_val "assertion" vc_label >> VC_Single ||
     scan_val "examine" vc_labels >> VC_Examine ||
-    scan_val "take" ((OuterParse.list vc_paths >> flat) -- Scan.option (
+    scan_val "take" ((Parse.list vc_paths >> flat) -- Scan.option (
       scan_val "without" vc_labels >> pair false ||
       scan_val "and_also" vc_labels >> pair true) >> VC_Take) ||
     scan_val "only" vc_labels >> VC_Only ||
@@ -295,9 +295,9 @@
   Scan.succeed VC_Complete
 
 val _ =
-  OuterSyntax.command "boogie_vc"
+  Outer_Syntax.command "boogie_vc"
     "Enter into proof mode for a specific verification condition."
-    OuterKeyword.thy_goal
+    Keyword.thy_goal
     (vc_name -- vc_opts >> (fn args =>
       (Toplevel.print o Toplevel.theory_to_proof (boogie_vc args))))
 
@@ -305,7 +305,7 @@
 val quick_timeout = 5
 val default_timeout = 20
 
-fun timeout name = Scan.optional (scan_val name OuterParse.nat)
+fun timeout name = Scan.optional (scan_val name Parse.nat)
 
 val status_test =
   scan_arg (
@@ -328,18 +328,18 @@
   f (Toplevel.theory_of state))
 
 val _ =
-  OuterSyntax.improper_command "boogie_status"
+  Outer_Syntax.improper_command "boogie_status"
     "Show the name and state of all loaded verification conditions."
-    OuterKeyword.diag
+    Keyword.diag
     (status_test >> status_cmd ||
      status_vc >> status_cmd ||
      Scan.succeed (status_cmd boogie_status))
 
 
 val _ =
-  OuterSyntax.command "boogie_end"
+  Outer_Syntax.command "boogie_end"
     "Close the current Boogie environment."
-    OuterKeyword.thy_decl
+    Keyword.thy_decl
     (Scan.succeed (Toplevel.theory boogie_end))
 
 
diff -r f5417836dbea -r 01594f816e3a src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Mon May 17 23:54:15 2010 +0200
@@ -3310,13 +3310,13 @@
   by auto
 
 method_setup approximation = {*
-  Scan.lift (OuterParse.nat)
+  Scan.lift Parse.nat
   --
   Scan.optional (Scan.lift (Args.$$$ "splitting" |-- Args.colon)
-    |-- OuterParse.and_list' (free --| Scan.lift (Args.$$$ "=") -- Scan.lift OuterParse.nat)) []
+    |-- Parse.and_list' (free --| Scan.lift (Args.$$$ "=") -- Scan.lift Parse.nat)) []
   --
   Scan.option (Scan.lift (Args.$$$ "taylor" |-- Args.colon)
-    |-- (free |-- Scan.lift (Args.$$$ "=") |-- Scan.lift OuterParse.nat))
+    |-- (free |-- Scan.lift (Args.$$$ "=") |-- Scan.lift Parse.nat))
   >>
   (fn ((prec, splitting), taylor) => fn ctxt =>
     SIMPLE_METHOD' (fn i =>
diff -r f5417836dbea -r 01594f816e3a src/HOL/Import/import_syntax.ML
--- a/src/HOL/Import/import_syntax.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Import/import_syntax.ML	Mon May 17 23:54:15 2010 +0200
@@ -28,25 +28,23 @@
 structure HOL4ImportSyntax :> HOL4_IMPORT_SYNTAX =
 struct
 
-local structure P = OuterParse and K = OuterKeyword in
-
 (* Parsers *)
 
-val import_segment = P.name >> set_import_segment
+val import_segment = Parse.name >> set_import_segment
 
 
-val import_theory = P.name >> (fn thyname =>
+val import_theory = Parse.name >> (fn thyname =>
                                fn thy =>
                                   thy |> set_generating_thy thyname
                                       |> Sign.add_path thyname
                                       |> add_dump (";setup_theory " ^ thyname))
 
 fun do_skip_import_dir s = (ImportRecorder.set_skip_import_dir (SOME s); I)
-val skip_import_dir = P.string >> do_skip_import_dir
+val skip_import_dir = Parse.string >> do_skip_import_dir
 
 val lower = String.map Char.toLower
 fun do_skip_import s = (ImportRecorder.set_skip_import (case lower s of "on" => true | "off" => false | _ => Scan.fail ()); I)
-val skip_import = P.short_ident >> do_skip_import
+val skip_import = Parse.short_ident >> do_skip_import
 
 fun end_import toks =
     Scan.succeed
@@ -78,7 +76,7 @@
                     |> add_dump ";end_setup"
             end) toks
 
-val ignore_thms = Scan.repeat1 P.name
+val ignore_thms = Scan.repeat1 Parse.name
                                >> (fn ignored =>
                                    fn thy =>
                                       let
@@ -87,7 +85,7 @@
                                           Library.foldl (fn (thy,thmname) => ignore_hol4 thyname thmname thy) (thy,ignored)
                                       end)
 
-val thm_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname)
+val thm_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)
                             >> (fn thmmaps =>
                                 fn thy =>
                                    let
@@ -96,7 +94,7 @@
                                        Library.foldl (fn (thy,(hol,isa)) => add_hol4_mapping thyname hol isa thy) (thy,thmmaps)
                                    end)
 
-val type_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname)
+val type_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)
                              >> (fn typmaps =>
                                  fn thy =>
                                     let
@@ -105,7 +103,7 @@
                                         Library.foldl (fn (thy,(hol,isa)) => add_hol4_type_mapping thyname hol false isa thy) (thy,typmaps)
                                     end)
 
-val def_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname)
+val def_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)
                             >> (fn defmaps =>
                                 fn thy =>
                                    let
@@ -114,7 +112,7 @@
                                        Library.foldl (fn (thy,(hol,isa)) => add_defmap thyname hol isa thy) (thy,defmaps)
                                    end)
 
-val const_renames = Scan.repeat1 (P.name --| P.$$$ ">" -- P.name)
+val const_renames = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.name)
                                  >> (fn renames =>
                                      fn thy =>
                                         let
@@ -123,7 +121,7 @@
                                             Library.foldl (fn (thy,(hol,isa)) => add_hol4_const_renaming thyname hol isa thy) (thy,renames)
                                         end)
                                                                                                                                       
-val const_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
+val const_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname -- Scan.option (Parse.$$$ "::" |-- Parse.typ))
                               >> (fn constmaps =>
                                   fn thy =>
                                      let
@@ -133,7 +131,7 @@
                                                  | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol false isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps)
                                      end)
 
-val const_moves = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
+val const_moves = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname -- Scan.option (Parse.$$$ "::" |-- Parse.typ))
                                >> (fn constmaps =>
                                    fn thy =>
                                       let
@@ -156,16 +154,16 @@
         val get_lexes = fn () => !lexes
         val token_source = Token.source {do_recover = NONE} get_lexes Position.start symb_source
         val token_list = filter_out (Token.is_kind Token.Space) (Source.exhaust token_source)
-        val import_segmentP = OuterParse.$$$ "import_segment" |-- import_segment
-        val type_mapsP = OuterParse.$$$ "type_maps" |-- type_maps
-        val def_mapsP = OuterParse.$$$ "def_maps" |-- def_maps
-        val const_mapsP = OuterParse.$$$ "const_maps" |-- const_maps
-        val const_movesP = OuterParse.$$$ "const_moves" |-- const_moves
-        val const_renamesP = OuterParse.$$$ "const_renames" |-- const_renames
-        val ignore_thmsP = OuterParse.$$$ "ignore_thms" |-- ignore_thms
-        val thm_mapsP = OuterParse.$$$ "thm_maps" |-- thm_maps
+        val import_segmentP = Parse.$$$ "import_segment" |-- import_segment
+        val type_mapsP = Parse.$$$ "type_maps" |-- type_maps
+        val def_mapsP = Parse.$$$ "def_maps" |-- def_maps
+        val const_mapsP = Parse.$$$ "const_maps" |-- const_maps
+        val const_movesP = Parse.$$$ "const_moves" |-- const_moves
+        val const_renamesP = Parse.$$$ "const_renames" |-- const_renames
+        val ignore_thmsP = Parse.$$$ "ignore_thms" |-- ignore_thms
+        val thm_mapsP = Parse.$$$ "thm_maps" |-- thm_maps
         val parser = type_mapsP || def_mapsP || const_mapsP || const_movesP || const_renamesP || thm_mapsP || ignore_thmsP || import_segmentP
-        val importP = OuterParse.$$$ "import" |-- Scan.repeat parser --| OuterParse.$$$ "end"
+        val importP = Parse.$$$ "import" |-- Scan.repeat parser --| Parse.$$$ "end"
         fun apply [] thy = thy
           | apply (f::fs) thy = apply fs (f thy)
     in
@@ -188,7 +186,7 @@
             NONE => error "Import data already cleared - forgotten a setup_theory?"
           | SOME _ => ImportData.put NONE thy
 
-val setup_theory = P.name
+val setup_theory = Parse.name
                        >>
                        (fn thyname =>
                         fn thy =>
@@ -212,64 +210,62 @@
                     |> Sign.parent_path
             end) toks
 
-val set_dump  = P.string -- P.string   >> setup_dump
+val set_dump  = Parse.string -- Parse.string   >> setup_dump
 fun fl_dump toks  = Scan.succeed flush_dump toks
-val append_dump = (P.verbatim || P.string) >> add_dump
+val append_dump = (Parse.verbatim || Parse.string) >> add_dump
 
 fun setup () =
-  (OuterKeyword.keyword ">";
-   OuterSyntax.command "import_segment"
+  (Keyword.keyword ">";
+   Outer_Syntax.command "import_segment"
                        "Set import segment name"
-                       K.thy_decl (import_segment >> Toplevel.theory);
-   OuterSyntax.command "import_theory"
+                       Keyword.thy_decl (import_segment >> Toplevel.theory);
+   Outer_Syntax.command "import_theory"
                        "Set default HOL4 theory name"
-                       K.thy_decl (import_theory >> Toplevel.theory);
-   OuterSyntax.command "end_import"
+                       Keyword.thy_decl (import_theory >> Toplevel.theory);
+   Outer_Syntax.command "end_import"
                        "End HOL4 import"
-                       K.thy_decl (end_import >> Toplevel.theory);
-   OuterSyntax.command "skip_import_dir" 
+                       Keyword.thy_decl (end_import >> Toplevel.theory);
+   Outer_Syntax.command "skip_import_dir" 
                        "Sets caching directory for skipping importing"
-                       K.thy_decl (skip_import_dir >> Toplevel.theory);
-   OuterSyntax.command "skip_import" 
+                       Keyword.thy_decl (skip_import_dir >> Toplevel.theory);
+   Outer_Syntax.command "skip_import" 
                        "Switches skipping importing on or off"
-                       K.thy_decl (skip_import >> Toplevel.theory);                   
-   OuterSyntax.command "setup_theory"
+                       Keyword.thy_decl (skip_import >> Toplevel.theory);                   
+   Outer_Syntax.command "setup_theory"
                        "Setup HOL4 theory replaying"
-                       K.thy_decl (setup_theory >> Toplevel.theory);
-   OuterSyntax.command "end_setup"
+                       Keyword.thy_decl (setup_theory >> Toplevel.theory);
+   Outer_Syntax.command "end_setup"
                        "End HOL4 setup"
-                       K.thy_decl (end_setup >> Toplevel.theory);
-   OuterSyntax.command "setup_dump"
+                       Keyword.thy_decl (end_setup >> Toplevel.theory);
+   Outer_Syntax.command "setup_dump"
                        "Setup the dump file name"
-                       K.thy_decl (set_dump >> Toplevel.theory);
-   OuterSyntax.command "append_dump"
+                       Keyword.thy_decl (set_dump >> Toplevel.theory);
+   Outer_Syntax.command "append_dump"
                        "Add text to dump file"
-                       K.thy_decl (append_dump >> Toplevel.theory);
-   OuterSyntax.command "flush_dump"
+                       Keyword.thy_decl (append_dump >> Toplevel.theory);
+   Outer_Syntax.command "flush_dump"
                        "Write the dump to file"
-                       K.thy_decl (fl_dump >> Toplevel.theory);
-   OuterSyntax.command "ignore_thms"
+                       Keyword.thy_decl (fl_dump >> Toplevel.theory);
+   Outer_Syntax.command "ignore_thms"
                        "Theorems to ignore in next HOL4 theory import"
-                       K.thy_decl (ignore_thms >> Toplevel.theory);
-   OuterSyntax.command "type_maps"
+                       Keyword.thy_decl (ignore_thms >> Toplevel.theory);
+   Outer_Syntax.command "type_maps"
                        "Map HOL4 type names to existing Isabelle/HOL type names"
-                       K.thy_decl (type_maps >> Toplevel.theory);
-   OuterSyntax.command "def_maps"
+                       Keyword.thy_decl (type_maps >> Toplevel.theory);
+   Outer_Syntax.command "def_maps"
                        "Map HOL4 constant names to their primitive definitions"
-                       K.thy_decl (def_maps >> Toplevel.theory);
-   OuterSyntax.command "thm_maps"
+                       Keyword.thy_decl (def_maps >> Toplevel.theory);
+   Outer_Syntax.command "thm_maps"
                        "Map HOL4 theorem names to existing Isabelle/HOL theorem names"
-                       K.thy_decl (thm_maps >> Toplevel.theory);
-   OuterSyntax.command "const_renames"
+                       Keyword.thy_decl (thm_maps >> Toplevel.theory);
+   Outer_Syntax.command "const_renames"
                        "Rename HOL4 const names"
-                       K.thy_decl (const_renames >> Toplevel.theory);
-   OuterSyntax.command "const_moves"
+                       Keyword.thy_decl (const_renames >> Toplevel.theory);
+   Outer_Syntax.command "const_moves"
                        "Rename HOL4 const names to other HOL4 constants"
-                       K.thy_decl (const_moves >> Toplevel.theory);
-   OuterSyntax.command "const_maps"
+                       Keyword.thy_decl (const_moves >> Toplevel.theory);
+   Outer_Syntax.command "const_maps"
                        "Map HOL4 const names to existing Isabelle/HOL const names"
-                       K.thy_decl (const_maps >> Toplevel.theory));
+                       Keyword.thy_decl (const_maps >> Toplevel.theory));
 
 end
-
-end
diff -r f5417836dbea -r 01594f816e3a src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Mon May 17 23:54:15 2010 +0200
@@ -189,7 +189,7 @@
   else Delimfix (Syntax.escape c)
 
 fun quotename c =
-  if Syntax.is_identifier c andalso not (OuterKeyword.is_keyword c) then c else quote c
+  if Syntax.is_identifier c andalso not (Keyword.is_keyword c) then c else quote c
 
 fun simple_smart_string_of_cterm ct =
     let
diff -r f5417836dbea -r 01594f816e3a src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML
--- a/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Mon May 17 23:54:15 2010 +0200
@@ -144,11 +144,11 @@
 
 val setup =
   Method.setup @{binding sos}
-    (Scan.lift (Scan.option OuterParse.xname)
+    (Scan.lift (Scan.option Parse.xname)
       >> (sos_solver print_cert o Sum_Of_Squares.Prover o call_solver))
     "prove universal problems over the reals using sums of squares" #>
   Method.setup @{binding sos_cert}
-    (Scan.lift OuterParse.string
+    (Scan.lift Parse.string
       >> (fn cert => fn ctxt =>
         sos_solver ignore
           (Sum_Of_Squares.Certificate (PositivstellensatzTools.cert_to_pss_tree ctxt cert)) ctxt))
diff -r f5417836dbea -r 01594f816e3a src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon May 17 23:54:15 2010 +0200
@@ -330,7 +330,7 @@
 
 fun thms_of_name ctxt name =
   let
-    val lex = OuterKeyword.get_lexicons
+    val lex = Keyword.get_lexicons
     val get = maps (ProofContext.get_fact ctxt o fst)
   in
     Source.of_string name
diff -r f5417836dbea -r 01594f816e3a src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Mon May 17 23:54:15 2010 +0200
@@ -1004,10 +1004,10 @@
 
 
 (* syntax und parsing *)
-structure P = OuterParse and K = OuterKeyword;
+structure P = Parse and K = Keyword;
 
 val _ =
-  OuterSyntax.command "atom_decl" "Declare new kinds of atoms" K.thy_decl
-    (Scan.repeat1 P.name >> (Toplevel.theory o create_nom_typedecls));
+  Outer_Syntax.command "atom_decl" "declare new kinds of atoms" Keyword.thy_decl
+    (Scan.repeat1 Parse.name >> (Toplevel.theory o create_nom_typedecls));
 
 end;
diff -r f5417836dbea -r 01594f816e3a src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Mon May 17 23:54:15 2010 +0200
@@ -2076,11 +2076,10 @@
 
 (* FIXME: The following stuff should be exported by Datatype *)
 
-local structure P = OuterParse and K = OuterKeyword in
-
 val datatype_decl =
-  Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_mixfix --
-    (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
+  Scan.option (Parse.$$$ "(" |-- Parse.name --| Parse.$$$ ")") --
+    Parse.type_args -- Parse.name -- Parse.opt_mixfix --
+    (Parse.$$$ "=" |-- Parse.enum1 "|" (Parse.name -- Scan.repeat Parse.typ -- Parse.opt_mixfix));
 
 fun mk_datatype args =
   let
@@ -2090,9 +2089,7 @@
   in add_nominal_datatype Datatype.default_config names specs end;
 
 val _ =
-  OuterSyntax.command "nominal_datatype" "define inductive datatypes" K.thy_decl
-    (P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
-
-end;
+  Outer_Syntax.command "nominal_datatype" "define inductive datatypes" Keyword.thy_decl
+    (Parse.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
 
 end
diff -r f5417836dbea -r 01594f816e3a src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML	Mon May 17 23:54:15 2010 +0200
@@ -138,8 +138,6 @@
 
 local
 
-structure P = OuterParse;
-
 val avoidingN = "avoiding";
 val fixingN = "arbitrary";  (* to be consistent with induct; hopefully this changes again *)
 val ruleN = "rule";
@@ -165,14 +163,14 @@
   Scan.repeat (unless_more_args free)) [];
 
 val fixing = Scan.optional (Scan.lift (Args.$$$ fixingN -- Args.colon) |--
-  P.and_list' (Scan.repeat (unless_more_args free))) [];
+  Parse.and_list' (Scan.repeat (unless_more_args free))) [];
 
 val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thms;
 
 in
 
 val nominal_induct_method =
-  Args.mode Induct.no_simpN -- (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
+  Args.mode Induct.no_simpN -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
   avoiding -- fixing -- rule_spec) >>
   (fn (no_simp, (((x, y), z), w)) => fn ctxt =>
     RAW_METHOD_CASES (fn facts =>
diff -r f5417836dbea -r 01594f816e3a src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Mon May 17 23:54:15 2010 +0200
@@ -672,23 +672,20 @@
 
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterKeyword in
-
-val _ = OuterKeyword.keyword "avoids";
+val _ = Keyword.keyword "avoids";
 
 val _ =
-  OuterSyntax.local_theory_to_proof "nominal_inductive"
-    "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal
-    (P.xname -- Scan.optional (P.$$$ "avoids" |-- P.and_list1 (P.name --
-      (P.$$$ ":" |-- Scan.repeat1 P.name))) [] >> (fn (name, avoids) =>
+  Outer_Syntax.local_theory_to_proof "nominal_inductive"
+    "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes"
+    Keyword.thy_goal
+    (Parse.xname -- Scan.optional (Parse.$$$ "avoids" |-- Parse.and_list1 (Parse.name --
+      (Parse.$$$ ":" |-- Scan.repeat1 Parse.name))) [] >> (fn (name, avoids) =>
         prove_strong_ind name avoids));
 
 val _ =
-  OuterSyntax.local_theory "equivariance"
-    "prove equivariance for inductive predicate involving nominal datatypes" K.thy_decl
-    (P.xname -- Scan.optional (P.$$$ "[" |-- P.list1 P.name --| P.$$$ "]") [] >>
+  Outer_Syntax.local_theory "equivariance"
+    "prove equivariance for inductive predicate involving nominal datatypes" Keyword.thy_decl
+    (Parse.xname -- Scan.optional (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]") [] >>
       (fn (name, atoms) => prove_eqvt name atoms));
 
-end;
-
 end
diff -r f5417836dbea -r 01594f816e3a src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Mon May 17 23:54:15 2010 +0200
@@ -485,17 +485,14 @@
 
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterKeyword in
-
 val _ =
-  OuterSyntax.local_theory_to_proof "nominal_inductive2"
-    "prove strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal
-    (P.xname -- 
-     Scan.option (P.$$$ "(" |-- P.!!! (P.name --| P.$$$ ")")) --
-     (Scan.optional (P.$$$ "avoids" |-- P.enum1 "|" (P.name --
-      (P.$$$ ":" |-- P.and_list1 P.term))) []) >> (fn ((name, rule_name), avoids) =>
+  Outer_Syntax.local_theory_to_proof "nominal_inductive2"
+    "prove strong induction theorem for inductive predicate involving nominal datatypes"
+    Keyword.thy_goal
+    (Parse.xname -- 
+     Scan.option (Parse.$$$ "(" |-- Parse.!!! (Parse.name --| Parse.$$$ ")")) --
+     (Scan.optional (Parse.$$$ "avoids" |-- Parse.enum1 "|" (Parse.name --
+      (Parse.$$$ ":" |-- Parse.and_list1 Parse.term))) []) >> (fn ((name, rule_name), avoids) =>
         prove_strong_ind name rule_name avoids));
 
-end;
-
 end
diff -r f5417836dbea -r 01594f816e3a src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML	Mon May 17 23:54:15 2010 +0200
@@ -393,28 +393,24 @@
 
 (* outer syntax *)
 
-local structure P = OuterParse in
-
-val freshness_context = P.reserved "freshness_context";
-val invariant = P.reserved "invariant";
+val freshness_context = Parse.reserved "freshness_context";
+val invariant = Parse.reserved "invariant";
 
-fun unless_flag scan = Scan.unless ((freshness_context || invariant) -- P.$$$ ":") scan;
+fun unless_flag scan = Scan.unless ((freshness_context || invariant) -- Parse.$$$ ":") scan;
 
-val parser1 = (freshness_context -- P.$$$ ":") |-- unless_flag P.term >> SOME;
-val parser2 = (invariant -- P.$$$ ":") |--
-    (Scan.repeat1 (unless_flag P.term) >> SOME) -- Scan.optional parser1 NONE ||
+val parser1 = (freshness_context -- Parse.$$$ ":") |-- unless_flag Parse.term >> SOME;
+val parser2 = (invariant -- Parse.$$$ ":") |--
+    (Scan.repeat1 (unless_flag Parse.term) >> SOME) -- Scan.optional parser1 NONE ||
   (parser1 >> pair NONE);
 val options =
-  Scan.optional (P.$$$ "(" |-- P.!!! (parser2 --| P.$$$ ")")) (NONE, NONE);
+  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (parser2 --| Parse.$$$ ")")) (NONE, NONE);
 
 val _ =
-  OuterSyntax.local_theory_to_proof "nominal_primrec"
-    "define primitive recursive functions on nominal datatypes" OuterKeyword.thy_goal
-    (options -- P.fixes -- P.for_fixes -- Parse_Spec.where_alt_specs
+  Outer_Syntax.local_theory_to_proof "nominal_primrec"
+    "define primitive recursive functions on nominal datatypes" Keyword.thy_goal
+    (options -- Parse.fixes -- Parse.for_fixes -- Parse_Spec.where_alt_specs
       >> (fn ((((invs, fctxt), fixes), params), specs) =>
         add_primrec_cmd invs fctxt fixes params specs));
 
 end;
 
-end;
-
diff -r f5417836dbea -r 01594f816e3a src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Orderings.thy	Mon May 17 23:54:15 2010 +0200
@@ -422,8 +422,8 @@
 (** Diagnostic command **)
 
 val _ =
-  OuterSyntax.improper_command "print_orders"
-    "print order structures available to transitivity reasoner" OuterKeyword.diag
+  Outer_Syntax.improper_command "print_orders"
+    "print order structures available to transitivity reasoner" Keyword.diag
     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
         Toplevel.keep (print_structures o Toplevel.context_of)));
 
diff -r f5417836dbea -r 01594f816e3a src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML	Mon May 17 23:54:15 2010 +0200
@@ -667,37 +667,33 @@
 
 (*** outer syntax *)
 
-local structure P = OuterParse and K = OuterKeyword in
-
 val type_insts =
-  P.typ >> single ||
-  P.$$$ "(" |-- P.!!! (P.list1 P.typ --| P.$$$ ")")
+  Parse.typ >> single ||
+  Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.typ --| Parse.$$$ ")")
 
-val comp = P.name -- (P.$$$ "::" |-- P.!!! P.typ);
+val comp = Parse.name -- (Parse.$$$ "::" |-- Parse.!!! Parse.typ);
 fun plus1_unless test scan =
-  scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
+  scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan));
 
-val mapsto = P.$$$ "=";
-val rename = P.name -- (mapsto |-- P.name);
-val renames =  Scan.optional (P.$$$ "[" |-- P.!!! (P.list1 rename --| P.$$$ "]")) [];
+val mapsto = Parse.$$$ "=";
+val rename = Parse.name -- (mapsto |-- Parse.name);
+val renames = Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.list1 rename --| Parse.$$$ "]")) [];
 
 
-val parent = ((type_insts -- P.xname) || (P.xname >> pair [])) -- renames
+val parent = ((type_insts -- Parse.xname) || (Parse.xname >> pair [])) -- renames
              >> (fn ((insts,name),renames) => (insts,name,renames))
 
 
 val statespace_decl =
-   P.type_args -- P.name --
-    (P.$$$ "=" |--
+   Parse.type_args -- Parse.name --
+    (Parse.$$$ "=" |--
      ((Scan.repeat1 comp >> pair []) ||
       (plus1_unless comp parent --
-        Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 comp)) [])))
+        Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 comp)) [])))
 
 val statespace_command =
-  OuterSyntax.command "statespace" "define state space" K.thy_decl
+  Outer_Syntax.command "statespace" "define state space" Keyword.thy_decl
   (statespace_decl >> (fn ((args,name),(parents,comps)) =>
                            Toplevel.theory (define_statespace args name parents comps)))
 
-end;
-
 end;
\ No newline at end of file
diff -r f5417836dbea -r 01594f816e3a src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Mon May 17 23:54:15 2010 +0200
@@ -721,8 +721,6 @@
 
 local
 
-structure P = OuterParse and K = OuterKeyword
-
 fun prep_datatype_decls args =
   let
     val names = map
@@ -732,15 +730,16 @@
   in (names, specs) end;
 
 val parse_datatype_decl =
-  (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_mixfix --
-    (P.$$$ "=" |-- P.enum1 "|" (P.binding -- Scan.repeat P.typ -- P.opt_mixfix)));
+  (Scan.option (Parse.$$$ "(" |-- Parse.name --| Parse.$$$ ")") --
+    Parse.type_args -- Parse.binding -- Parse.opt_mixfix --
+    (Parse.$$$ "=" |-- Parse.enum1 "|" (Parse.binding -- Scan.repeat Parse.typ -- Parse.opt_mixfix)));
 
-val parse_datatype_decls = P.and_list1 parse_datatype_decl >> prep_datatype_decls;
+val parse_datatype_decls = Parse.and_list1 parse_datatype_decl >> prep_datatype_decls;
 
 in
 
 val _ =
-  OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl
+  Outer_Syntax.command "datatype" "define inductive datatypes" Keyword.thy_decl
     (parse_datatype_decls >> (fn (names, specs) => Toplevel.theory (datatype_cmd names specs)));
 
 end;
diff -r f5417836dbea -r 01594f816e3a src/HOL/Tools/Datatype/datatype_data.ML
--- a/src/HOL/Tools/Datatype/datatype_data.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Mon May 17 23:54:15 2010 +0200
@@ -455,18 +455,11 @@
 
 (* outer syntax *)
 
-local
-
-structure P = OuterParse and K = OuterKeyword
-
-in
-
 val _ =
-  OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_goal
-    (Scan.option (P.$$$ "(" |-- Scan.repeat1 P.name --| P.$$$ ")") -- Scan.repeat1 P.term
-      >> (fn (alt_names, ts) => Toplevel.print
-           o Toplevel.theory_to_proof (rep_datatype_cmd alt_names ts)));
+  Outer_Syntax.command "rep_datatype" "represent existing types inductively" Keyword.thy_goal
+    (Scan.option (Parse.$$$ "(" |-- Scan.repeat1 Parse.name --| Parse.$$$ ")") --
+      Scan.repeat1 Parse.term
+      >> (fn (alt_names, ts) =>
+        Toplevel.print o Toplevel.theory_to_proof (rep_datatype_cmd alt_names ts)));
 
 end;
-
-end;
diff -r f5417836dbea -r 01594f816e3a src/HOL/Tools/Function/fun.ML
--- a/src/HOL/Tools/Function/fun.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/Function/fun.ML	Mon May 17 23:54:15 2010 +0200
@@ -159,13 +159,10 @@
 
 
 
-local structure P = OuterParse and K = OuterKeyword in
-
 val _ =
-  OuterSyntax.local_theory "fun" "define general recursive functions (short version)" K.thy_decl
+  Outer_Syntax.local_theory "fun" "define general recursive functions (short version)"
+  Keyword.thy_decl
   (function_parser fun_config
-     >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config));
+     >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config))
 
 end
-
-end
diff -r f5417836dbea -r 01594f816e3a src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/Function/function.ML	Mon May 17 23:54:15 2010 +0200
@@ -274,20 +274,19 @@
 fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t
   |> the_single |> snd
 
+
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterKeyword in
-
 val _ =
-  OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal
+  Outer_Syntax.local_theory_to_proof "function" "define general recursive functions"
+  Keyword.thy_goal
   (function_parser default_config
      >> (fn ((config, fixes), statements) => function_cmd fixes statements config))
 
 val _ =
-  OuterSyntax.local_theory_to_proof "termination" "prove termination of a recursive function" K.thy_goal
-  (Scan.option P.term >> termination_cmd)
-
-end
+  Outer_Syntax.local_theory_to_proof "termination" "prove termination of a recursive function"
+  Keyword.thy_goal
+  (Scan.option Parse.term >> termination_cmd)
 
 
 end
diff -r f5417836dbea -r 01594f816e3a src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Mon May 17 23:54:15 2010 +0200
@@ -341,21 +341,19 @@
 
 
 local
-  structure P = OuterParse and K = OuterKeyword
-
-  val option_parser = P.group "option"
-    ((P.reserved "sequential" >> K Sequential)
-     || ((P.reserved "default" |-- P.term) >> Default)
-     || (P.reserved "domintros" >> K DomIntros)
-     || (P.reserved "no_partials" >> K No_Partials)
-     || (P.reserved "tailrec" >> K Tailrec))
+  val option_parser = Parse.group "option"
+    ((Parse.reserved "sequential" >> K Sequential)
+     || ((Parse.reserved "default" |-- Parse.term) >> Default)
+     || (Parse.reserved "domintros" >> K DomIntros)
+     || (Parse.reserved "no_partials" >> K No_Partials)
+     || (Parse.reserved "tailrec" >> K Tailrec))
 
   fun config_parser default =
-    (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 option_parser) --| P.$$$ ")") [])
+    (Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 option_parser) --| Parse.$$$ ")") [])
      >> (fn opts => fold apply_opt opts default)
 in
   fun function_parser default_cfg =
-      config_parser default_cfg -- P.fixes -- Parse_Spec.where_alt_specs
+      config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs
 end
 
 
diff -r f5417836dbea -r 01594f816e3a src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon May 17 23:54:15 2010 +0200
@@ -24,8 +24,6 @@
 open Nitpick_Nut
 open Nitpick
 
-structure K = OuterKeyword and P = OuterParse
-
 val auto = Unsynchronized.ref false;
 
 val _ =
@@ -289,14 +287,14 @@
   extract_params (ProofContext.init_global thy) false (default_raw_params thy)
   o map (apsnd single)
 
-val parse_key = Scan.repeat1 P.typ_group >> space_implode " "
+val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
 val parse_value =
-  Scan.repeat1 (P.minus >> single
-                || Scan.repeat1 (Scan.unless P.minus P.name)
-                || P.$$$ "," |-- P.number >> prefix "," >> single) >> flat
-val parse_param = parse_key -- Scan.optional (P.$$$ "=" |-- parse_value) []
+  Scan.repeat1 (Parse.minus >> single
+                || Scan.repeat1 (Scan.unless Parse.minus Parse.name)
+                || Parse.$$$ "," |-- Parse.number >> prefix "," >> single) >> flat
+val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
 val parse_params =
-  Scan.optional (P.$$$ "[" |-- P.list parse_param --| P.$$$ "]") []
+  Scan.optional (Parse.$$$ "[" |-- Parse.list parse_param --| Parse.$$$ "]") []
 
 fun handle_exceptions ctxt f x =
   f x
@@ -375,15 +373,15 @@
                                       |> sort_strings |> cat_lines)))))
 
 val parse_nitpick_command =
-  (parse_params -- Scan.optional P.nat 1) #>> nitpick_trans
+  (parse_params -- Scan.optional Parse.nat 1) #>> nitpick_trans
 val parse_nitpick_params_command = parse_params #>> nitpick_params_trans
 
-val _ = OuterSyntax.improper_command "nitpick"
+val _ = Outer_Syntax.improper_command "nitpick"
             "try to find a counterexample for a given subgoal using Nitpick"
-            K.diag parse_nitpick_command
-val _ = OuterSyntax.command "nitpick_params"
+            Keyword.diag parse_nitpick_command
+val _ = Outer_Syntax.command "nitpick_params"
             "set and display the default parameters for Nitpick"
-            K.thy_decl parse_nitpick_params_command
+            Keyword.thy_decl parse_nitpick_params_command
 
 fun auto_nitpick state =
   if not (!auto) then (false, state) else pick_nits [] true 1 0 state
diff -r f5417836dbea -r 01594f816e3a src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon May 17 23:54:15 2010 +0200
@@ -192,8 +192,6 @@
 
 val setup = Predicate_Compile_Core.setup
 
-local structure P = OuterParse
-in
 
 (* Parser for mode annotations *)
 
@@ -207,15 +205,15 @@
   (parse_mode_tuple_expr --| Args.$$$ "=>" -- parse_mode_expr >> Fun || parse_mode_tuple_expr) xs
 
 val mode_and_opt_proposal = parse_mode_expr --
-  Scan.optional (Args.$$$ "as" |-- P.xname >> SOME) NONE
+  Scan.optional (Args.$$$ "as" |-- Parse.xname >> SOME) NONE
 
 val opt_modes =
-  Scan.optional (P.$$$ "(" |-- Args.$$$ "modes" |-- P.$$$ ":" |--
-    P.enum "," mode_and_opt_proposal --| P.$$$ ")" >> SOME) NONE
+  Scan.optional (Parse.$$$ "(" |-- Args.$$$ "modes" |-- Parse.$$$ ":" |--
+    Parse.enum "," mode_and_opt_proposal --| Parse.$$$ ")" >> SOME) NONE
 
 val opt_expected_modes =
-  Scan.optional (P.$$$ "(" |-- Args.$$$ "expected_modes" |-- P.$$$ ":" |--
-    P.enum "," parse_mode_expr --| P.$$$ ")" >> SOME) NONE
+  Scan.optional (Parse.$$$ "(" |-- Args.$$$ "expected_modes" |-- Parse.$$$ ":" |--
+    Parse.enum "," parse_mode_expr --| Parse.$$$ ")" >> SOME) NONE
 
 (* Parser for options *)
 
@@ -224,46 +222,46 @@
     val scan_bool_option = foldl1 (op ||) (map Args.$$$ bool_options)
     val scan_compilation = foldl1 (op ||) (map (fn (s, c) => Args.$$$ s >> K c) compilation_names)
   in
-    Scan.optional (P.$$$ "[" |-- Scan.optional scan_compilation Pred
-      -- P.enum "," scan_bool_option --| P.$$$ "]")
+    Scan.optional (Parse.$$$ "[" |-- Scan.optional scan_compilation Pred
+      -- Parse.enum "," scan_bool_option --| Parse.$$$ "]")
       (Pred, [])
   end
 
-val opt_print_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
+val opt_print_modes =
+  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
 
-val opt_mode = (P.$$$ "_" >> K NONE) || (parse_mode_expr >> SOME)
+val opt_mode = (Parse.$$$ "_" >> K NONE) || (parse_mode_expr >> SOME)
 
-val opt_param_modes = Scan.optional (P.$$$ "[" |-- Args.$$$ "mode" |-- P.$$$ ":" |--
-  P.enum ", " opt_mode --| P.$$$ "]" >> SOME) NONE
+val opt_param_modes = Scan.optional (Parse.$$$ "[" |-- Args.$$$ "mode" |-- Parse.$$$ ":" |--
+  Parse.enum ", " opt_mode --| Parse.$$$ "]" >> SOME) NONE
 
 val stats = Scan.optional (Args.$$$ "stats" >> K true) false
 
 val value_options =
   let
-    val expected_values = Scan.optional (Args.$$$ "expected" |-- P.term >> SOME) NONE
+    val expected_values = Scan.optional (Args.$$$ "expected" |-- Parse.term >> SOME) NONE
     val scan_compilation =
       Scan.optional
         (foldl1 (op ||)
-          (map (fn (s, c) => Args.$$$ s -- P.enum "," P.int >> (fn (_, ps) => (c, ps)))
+          (map (fn (s, c) => Args.$$$ s -- Parse.enum "," Parse.int >> (fn (_, ps) => (c, ps)))
             compilation_names))
         (Pred, [])
   in
-    Scan.optional (P.$$$ "[" |-- (expected_values -- stats) -- scan_compilation --| P.$$$ "]")
+    Scan.optional
+      (Parse.$$$ "[" |-- (expected_values -- stats) -- scan_compilation --| Parse.$$$ "]")
       ((NONE, false), (Pred, []))
   end
 
 (* code_pred command and values command *)
 
-val _ = OuterSyntax.local_theory_to_proof "code_pred"
+val _ = Outer_Syntax.local_theory_to_proof "code_pred"
   "prove equations for predicate specified by intro/elim rules"
-  OuterKeyword.thy_goal
-  (opt_expected_modes -- opt_modes -- scan_options -- P.term_group >> code_pred_cmd)
+  Keyword.thy_goal
+  (opt_expected_modes -- opt_modes -- scan_options -- Parse.term_group >> code_pred_cmd)
 
-val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag
-  (opt_print_modes -- opt_param_modes -- value_options -- Scan.optional P.nat ~1 -- P.term
+val _ = Outer_Syntax.improper_command "values" "enumerate and print comprehensions" Keyword.diag
+  (opt_print_modes -- opt_param_modes -- value_options -- Scan.optional Parse.nat ~1 -- Parse.term
     >> (fn ((((print_modes, param_modes), options), k), t) => Toplevel.keep
         (Predicate_Compile_Core.values_cmd print_modes param_modes options k t)));
 
 end
-
-end
diff -r f5417836dbea -r 01594f816e3a src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Mon May 17 23:54:15 2010 +0200
@@ -91,20 +91,15 @@
   quotient_def ((NONE, NoSyn), (Attrib.empty_binding,
     (Quotient_Term.quotient_lift_const qtys (b, t) ctxt, t))) ctxt
 
-local
-  structure P = OuterParse;
-in
-
-val quotdef_decl = (P.binding >> SOME) -- P.opt_mixfix' --| P.$$$ "where"
+val quotdef_decl = (Parse.binding >> SOME) -- Parse.opt_mixfix' --| Parse.$$$ "where"
 
 val quotdef_parser =
   Scan.optional quotdef_decl (NONE, NoSyn) -- 
-    P.!!! (Parse_Spec.opt_thm_name ":" -- (P.term --| P.$$$ "is" -- P.term))
-end
+    Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| Parse.$$$ "is" -- Parse.term))
 
 val _ =
-  OuterSyntax.local_theory "quotient_definition"
+  Outer_Syntax.local_theory "quotient_definition"
     "definition for constants over the quotient type"
-      OuterKeyword.thy_decl (quotdef_parser >> (snd oo quotdef_cmd))
+      Keyword.thy_decl (quotdef_parser >> (snd oo quotdef_cmd))
 
 end; (* structure *)
diff -r f5417836dbea -r 01594f816e3a src/HOL/Tools/Quotient/quotient_info.ML
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Mon May 17 23:54:15 2010 +0200
@@ -91,9 +91,9 @@
 
 val maps_attr_parser =
   Args.context -- Scan.lift
-    ((Args.name --| OuterParse.$$$ "=") --
-      (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," --
-        Args.name --| OuterParse.$$$ ")"))
+    ((Args.name --| Parse.$$$ "=") --
+      (Parse.$$$ "(" |-- Args.name --| Parse.$$$ "," --
+        Args.name --| Parse.$$$ ")"))
 
 val _ = Context.>> (Context.map_theory
   (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute)
@@ -278,8 +278,8 @@
 (* setup of the printing commands *)
 
 fun improper_command (pp_fn, cmd_name, descr_str) =
-  OuterSyntax.improper_command cmd_name descr_str
-    OuterKeyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of)))
+  Outer_Syntax.improper_command cmd_name descr_str
+    Keyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of)))
 
 val _ = map improper_command
   [(print_mapsinfo, "print_quotmaps", "prints out all map functions"),
diff -r f5417836dbea -r 01594f816e3a src/HOL/Tools/Quotient/quotient_typ.ML
--- a/src/HOL/Tools/Quotient/quotient_typ.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Mon May 17 23:54:15 2010 +0200
@@ -299,16 +299,16 @@
 end
 
 val quotspec_parser =
-    OuterParse.and_list1
-     ((OuterParse.type_args -- OuterParse.binding) --
-        OuterParse.opt_mixfix -- (OuterParse.$$$ "=" |-- OuterParse.typ) --
-         (OuterParse.$$$ "/" |-- OuterParse.term))
+    Parse.and_list1
+     ((Parse.type_args -- Parse.binding) --
+        Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) --
+         (Parse.$$$ "/" |-- Parse.term))
 
-val _ = OuterKeyword.keyword "/"
+val _ = Keyword.keyword "/"
 
 val _ =
-    OuterSyntax.local_theory_to_proof "quotient_type"
+    Outer_Syntax.local_theory_to_proof "quotient_type"
       "quotient type definitions (require equivalence proofs)"
-         OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd)
+         Keyword.thy_goal (quotspec_parser >> quotient_type_cmd)
 
 end; (* structure *)
diff -r f5417836dbea -r 01594f816e3a src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Mon May 17 23:54:15 2010 +0200
@@ -311,14 +311,14 @@
 
 val setup =
   Attrib.setup (Binding.name "smt_solver")
-    (Scan.lift (OuterParse.$$$ "=" |-- Args.name) >>
+    (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
       (Thm.declaration_attribute o K o select_solver))
     "SMT solver configuration" #>
   setup_timeout #>
   setup_trace #>
   setup_fixed_certificates #>
   Attrib.setup (Binding.name "smt_certificates")
-    (Scan.lift (OuterParse.$$$ "=" |-- Args.name) >>
+    (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
       (Thm.declaration_attribute o K o select_certificates))
     "SMT certificates" #>
   Method.setup (Binding.name "smt") smt_method
@@ -353,9 +353,9 @@
       Pretty.big_list "Solver-specific settings:" infos])
   end
 
-val _ = OuterSyntax.improper_command "smt_status"
-  "Show the available SMT solvers and the currently selected solver."
-  OuterKeyword.diag
+val _ =
+  Outer_Syntax.improper_command "smt_status"
+    "show the available SMT solvers and the currently selected solver" Keyword.diag
     (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
       print_setup (Context.Proof (Toplevel.context_of state)))))
 
diff -r f5417836dbea -r 01594f816e3a src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon May 17 23:54:15 2010 +0200
@@ -24,8 +24,6 @@
 open ATP_Systems
 open Sledgehammer_Fact_Minimizer
 
-structure K = OuterKeyword and P = OuterParse
-
 (** Proof method used in Isar proofs **)
 
 val neg_clausify_setup =
@@ -36,7 +34,7 @@
 (** Attribute for converting a theorem into clauses **)
 
 val parse_clausify_attribute : attribute context_parser =
-  Scan.lift OuterParse.nat
+  Scan.lift Parse.nat
   >> (fn i => Thm.rule_attribute (fn context => fn th =>
                   let val thy = Context.theory_of context in
                     Meson.make_meta_clause (nth (cnf_axiom thy th) i)
@@ -321,13 +319,13 @@
                                params |> map string_for_raw_param
                                       |> sort_strings |> cat_lines)))))
 
-val parse_key = Scan.repeat1 P.typ_group >> space_implode " "
-val parse_value = Scan.repeat1 P.xname
-val parse_param = parse_key -- Scan.optional (P.$$$ "=" |-- parse_value) []
-val parse_params = Scan.optional (Args.bracks (P.list parse_param)) []
+val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
+val parse_value = Scan.repeat1 Parse.xname
+val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
+val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
 val parse_fact_refs =
-  Scan.repeat1 (Scan.unless (P.name -- Args.colon)
-                            (P.xname -- Scan.option Attrib.thm_sel)
+  Scan.repeat1 (Scan.unless (Parse.name -- Args.colon)
+                            (Parse.xname -- Scan.option Attrib.thm_sel)
                 >> (fn (name, interval) =>
                        Facts.Named ((name, Position.none), interval)))
 val parse_relevance_chunk =
@@ -340,18 +338,18 @@
                               >> merge_relevance_overrides))
                 (add_to_relevance_override [])
 val parse_sledgehammer_command =
-  (Scan.optional P.short_ident runN -- parse_params -- parse_relevance_override
-   -- Scan.option P.nat) #>> sledgehammer_trans
+  (Scan.optional Parse.short_ident runN -- parse_params -- parse_relevance_override
+   -- Scan.option Parse.nat) #>> sledgehammer_trans
 val parse_sledgehammer_params_command =
   parse_params #>> sledgehammer_params_trans
 
 val _ =
-  OuterSyntax.improper_command sledgehammerN
-      "search for first-order proof using automatic theorem provers" K.diag
+  Outer_Syntax.improper_command sledgehammerN
+      "search for first-order proof using automatic theorem provers" Keyword.diag
       parse_sledgehammer_command
 val _ =
-  OuterSyntax.command sledgehammer_paramsN
-      "set and display the default parameters for Sledgehammer" K.thy_decl
+  Outer_Syntax.command sledgehammer_paramsN
+      "set and display the default parameters for Sledgehammer" Keyword.thy_decl
       parse_sledgehammer_params_command
 
 val setup =
diff -r f5417836dbea -r 01594f816e3a src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon May 17 23:54:15 2010 +0200
@@ -102,7 +102,7 @@
   let val s = unyxml y in
     y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso
            not (is_long_identifier (perhaps (try (unprefix "?")) s))) orelse
-           OuterKeyword.is_keyword s) ? quote
+           Keyword.is_keyword s) ? quote
   end
 
 fun monomorphic_term subst t =
diff -r f5417836dbea -r 01594f816e3a src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/choice_specification.ML	Mon May 17 23:54:15 2010 +0200
@@ -232,33 +232,28 @@
 
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterKeyword in
-
-val opt_name = Scan.optional (P.name --| P.$$$ ":") ""
-val opt_overloaded = P.opt_keyword "overloaded";
+val opt_name = Scan.optional (Parse.name --| Parse.$$$ ":") ""
+val opt_overloaded = Parse.opt_keyword "overloaded"
 
 val specification_decl =
-  P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
-          Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop)
+  Parse.$$$ "(" |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| Parse.$$$ ")" --
+          Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop)
 
 val _ =
-  OuterSyntax.command "specification" "define constants by specification" K.thy_goal
+  Outer_Syntax.command "specification" "define constants by specification" Keyword.thy_goal
     (specification_decl >> (fn (cos,alt_props) =>
                                Toplevel.print o (Toplevel.theory_to_proof
                                                      (process_spec NONE cos alt_props))))
 
 val ax_specification_decl =
-    P.name --
-    (P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
-           Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop))
+    Parse.name --
+    (Parse.$$$ "(" |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| Parse.$$$ ")" --
+           Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop))
 
 val _ =
-  OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal
+  Outer_Syntax.command "ax_specification" "define constants by specification" Keyword.thy_goal
     (ax_specification_decl >> (fn (axname,(cos,alt_props)) =>
                                Toplevel.print o (Toplevel.theory_to_proof
                                                      (process_spec (SOME axname) cos alt_props))))
 
 end
-
-
-end
diff -r f5417836dbea -r 01594f816e3a src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/inductive.ML	Mon May 17 23:54:15 2010 +0200
@@ -970,32 +970,28 @@
 
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterKeyword in
-
-val _ = OuterKeyword.keyword "monos";
+val _ = Keyword.keyword "monos";
 
 fun gen_ind_decl mk_def coind =
-  P.fixes -- P.for_fixes --
+  Parse.fixes -- Parse.for_fixes --
   Scan.optional Parse_Spec.where_alt_specs [] --
-  Scan.optional (P.$$$ "monos" |-- P.!!! Parse_Spec.xthms1) []
+  Scan.optional (Parse.$$$ "monos" |-- Parse.!!! Parse_Spec.xthms1) []
   >> (fn (((preds, params), specs), monos) =>
       (snd oo gen_add_inductive mk_def true coind preds params specs monos));
 
 val ind_decl = gen_ind_decl add_ind_def;
 
 val _ =
-  OuterSyntax.local_theory' "inductive" "define inductive predicates" K.thy_decl
+  Outer_Syntax.local_theory' "inductive" "define inductive predicates" Keyword.thy_decl
     (ind_decl false);
 
 val _ =
-  OuterSyntax.local_theory' "coinductive" "define coinductive predicates" K.thy_decl
+  Outer_Syntax.local_theory' "coinductive" "define coinductive predicates" Keyword.thy_decl
     (ind_decl true);
 
 val _ =
-  OuterSyntax.local_theory "inductive_cases"
-    "create simplified instances of elimination rules (improper)" K.thy_script
-    (P.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
+  Outer_Syntax.local_theory "inductive_cases"
+    "create simplified instances of elimination rules (improper)" Keyword.thy_script
+    (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
 
 end;
-
-end;
diff -r f5417836dbea -r 01594f816e3a src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Mon May 17 23:54:15 2010 +0200
@@ -775,7 +775,7 @@
   add_codegen "inductive" inductive_codegen #>
   Attrib.setup @{binding code_ind}
     (Scan.lift (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
-      Scan.option (Args.$$$ "params" |-- Args.colon |-- OuterParse.nat) >> uncurry add))
+      Scan.option (Args.$$$ "params" |-- Args.colon |-- Parse.nat) >> uncurry add))
     "introduction rules for executable predicates";
 
 (**** Quickcheck involving inductive predicates ****)
diff -r f5417836dbea -r 01594f816e3a src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Mon May 17 23:54:15 2010 +0200
@@ -562,18 +562,14 @@
 
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterKeyword in
-
 val ind_set_decl = Inductive.gen_ind_decl add_ind_set_def;
 
 val _ =
-  OuterSyntax.local_theory' "inductive_set" "define inductive sets" K.thy_decl
+  Outer_Syntax.local_theory' "inductive_set" "define inductive sets" Keyword.thy_decl
     (ind_set_decl false);
 
 val _ =
-  OuterSyntax.local_theory' "coinductive_set" "define coinductive sets" K.thy_decl
+  Outer_Syntax.local_theory' "coinductive_set" "define coinductive sets" Keyword.thy_decl
     (ind_set_decl true);
 
 end;
-
-end;
diff -r f5417836dbea -r 01594f816e3a src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/primrec.ML	Mon May 17 23:54:15 2010 +0200
@@ -307,29 +307,26 @@
 
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterKeyword in
-
 val opt_unchecked_name =
-  Scan.optional (P.$$$ "(" |-- P.!!!
-    (((P.$$$ "unchecked" >> K true) -- Scan.optional P.name "" ||
-      P.name >> pair false) --| P.$$$ ")")) (false, "");
+  Scan.optional (Parse.$$$ "(" |-- Parse.!!!
+    (((Parse.$$$ "unchecked" >> K true) -- Scan.optional Parse.name "" ||
+      Parse.name >> pair false) --| Parse.$$$ ")")) (false, "");
 
 val old_primrec_decl =
   opt_unchecked_name --
-    Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop);
+    Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop);
 
-val primrec_decl = P.opt_target -- P.fixes -- Parse_Spec.where_alt_specs;
+val primrec_decl = Parse.opt_target -- Parse.fixes -- Parse_Spec.where_alt_specs;
 
 val _ =
-  OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
+  Outer_Syntax.command "primrec" "define primitive recursive functions on datatypes"
+  Keyword.thy_decl
     ((primrec_decl >> (fn ((opt_target, fixes), specs) =>
       Toplevel.local_theory opt_target (add_primrec_cmd fixes specs #> snd)))
     || (old_primrec_decl >> (fn ((unchecked, alt_name), eqns) =>
       Toplevel.theory (snd o
         (if unchecked then OldPrimrec.add_primrec_unchecked else OldPrimrec.add_primrec)
-          alt_name (map P.triple_swap eqns) o
+          alt_name (map Parse.triple_swap eqns) o
         tap (fn _ => legacy_feature "Old variant of 'primrec' command -- use new syntax instead")))));
 
 end;
-
-end;
diff -r f5417836dbea -r 01594f816e3a src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/recdef.ML	Mon May 17 23:54:15 2010 +0200
@@ -289,40 +289,39 @@
 
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterKeyword in
-
-val _ = List.app OuterKeyword.keyword ["permissive", "congs", "hints"];
+val _ = List.app Keyword.keyword ["permissive", "congs", "hints"];
 
 val hints =
-  P.$$$ "(" |-- P.!!! (P.position (P.$$$ "hints" -- Args.parse) --| P.$$$ ")") >> Args.src;
+  Parse.$$$ "(" |--
+    Parse.!!! (Parse.position (Parse.$$$ "hints" -- Args.parse) --| Parse.$$$ ")") >> Args.src;
 
 val recdef_decl =
-  Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true --
-  P.name -- P.term -- Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- P.prop)
+  Scan.optional
+    (Parse.$$$ "(" -- Parse.!!! (Parse.$$$ "permissive" -- Parse.$$$ ")") >> K false) true --
+  Parse.name -- Parse.term -- Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)
     -- Scan.option hints
-  >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
+  >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map Parse.triple_swap eqs) src);
 
 val _ =
-  OuterSyntax.command "recdef" "define general recursive functions (TFL)" K.thy_decl
+  Outer_Syntax.command "recdef" "define general recursive functions (TFL)" Keyword.thy_decl
     (recdef_decl >> Toplevel.theory);
 
 
 val defer_recdef_decl =
-  P.name -- Scan.repeat1 P.prop --
-  Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (Parse_Spec.xthms1 --| P.$$$ ")")) []
+  Parse.name -- Scan.repeat1 Parse.prop --
+  Scan.optional
+    (Parse.$$$ "(" |-- Parse.$$$ "congs" |-- Parse.!!! (Parse_Spec.xthms1 --| Parse.$$$ ")")) []
   >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
 
 val _ =
-  OuterSyntax.command "defer_recdef" "defer general recursive functions (TFL)" K.thy_decl
+  Outer_Syntax.command "defer_recdef" "defer general recursive functions (TFL)" Keyword.thy_decl
     (defer_recdef_decl >> Toplevel.theory);
 
 val _ =
-  OuterSyntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
-    K.thy_goal
-    ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- P.xname --
-        Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
+  Outer_Syntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
+    Keyword.thy_goal
+    ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.xname --
+        Scan.option (Parse.$$$ "(" |-- Parse.nat --| Parse.$$$ ")")
       >> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
 
 end;
-
-end;
diff -r f5417836dbea -r 01594f816e3a src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/record.ML	Mon May 17 23:54:15 2010 +0200
@@ -2460,17 +2460,14 @@
 
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterKeyword in
-
 val _ =
-  OuterSyntax.command "record" "define extensible record" K.thy_decl
-    (P.type_args_constrained -- P.binding --
-      (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const_binding)
+  Outer_Syntax.command "record" "define extensible record" Keyword.thy_decl
+    (Parse.type_args_constrained -- Parse.binding --
+      (Parse.$$$ "=" |-- Scan.option (Parse.typ --| Parse.$$$ "+") --
+        Scan.repeat1 Parse.const_binding)
     >> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd false x y z)));
 
 end;
 
-end;
-
 structure Basic_Record: BASIC_RECORD = Record;
 open Basic_Record;
diff -r f5417836dbea -r 01594f816e3a src/HOL/Tools/refute_isar.ML
--- a/src/HOL/Tools/refute_isar.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/refute_isar.ML	Mon May 17 23:54:15 2010 +0200
@@ -12,19 +12,16 @@
 
 (*optional list of arguments of the form [name1=value1, name2=value2, ...]*)
 
-val scan_parm =
-  OuterParse.name
-  -- (Scan.optional (OuterParse.$$$ "=" |-- OuterParse.name) "true")
-val scan_parms = Scan.optional
-  (OuterParse.$$$ "[" |-- OuterParse.list scan_parm --| OuterParse.$$$ "]") [];
+val scan_parm = Parse.name -- (Scan.optional (Parse.$$$ "=" |-- Parse.name) "true")
+val scan_parms = Scan.optional (Parse.$$$ "[" |-- Parse.list scan_parm --| Parse.$$$ "]") [];
 
 
 (* 'refute' command *)
 
 val _ =
-  OuterSyntax.improper_command "refute"
-    "try to find a model that refutes a given subgoal" OuterKeyword.diag
-    (scan_parms -- Scan.optional OuterParse.nat 1 >>
+  Outer_Syntax.improper_command "refute"
+    "try to find a model that refutes a given subgoal" Keyword.diag
+    (scan_parms -- Scan.optional Parse.nat 1 >>
       (fn (parms, i) =>
         Toplevel.keep (fn state =>
           let
@@ -36,8 +33,8 @@
 (* 'refute_params' command *)
 
 val _ =
-  OuterSyntax.command "refute_params"
-    "show/store default parameters for the 'refute' command" OuterKeyword.thy_decl
+  Outer_Syntax.command "refute_params"
+    "show/store default parameters for the 'refute' command" Keyword.thy_decl
     (scan_parms >> (fn parms =>
       Toplevel.theory (fn thy =>
         let
diff -r f5417836dbea -r 01594f816e3a src/HOL/Tools/split_rule.ML
--- a/src/HOL/Tools/split_rule.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/split_rule.ML	Mon May 17 23:54:15 2010 +0200
@@ -135,7 +135,7 @@
   Attrib.setup @{binding split_format}
     (Scan.lift
      (Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule)) ||
-      OuterParse.and_list1 (Scan.repeat Args.name_source)
+      Parse.and_list1 (Scan.repeat Args.name_source)
         >> (fn xss => Thm.rule_attribute (fn context =>
             split_rule_goal (Context.proof_of context) xss))))
     "split pair-typed subterms in premises, or function arguments" #>
diff -r f5417836dbea -r 01594f816e3a src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/typedef.ML	Mon May 17 23:54:15 2010 +0200
@@ -296,22 +296,19 @@
 
 (** outer syntax **)
 
-local structure P = OuterParse in
-
-val _ = OuterKeyword.keyword "morphisms";
+val _ = Keyword.keyword "morphisms";
 
 val _ =
-  OuterSyntax.local_theory_to_proof "typedef" "HOL type definition (requires non-emptiness proof)"
-    OuterKeyword.thy_goal
-    (Scan.optional (P.$$$ "(" |--
-        ((P.$$$ "open" >> K false) -- Scan.option P.binding ||
-          P.binding >> (fn s => (true, SOME s))) --| P.$$$ ")") (true, NONE) --
-      (P.type_args_constrained -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) --
-      Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding))
+  Outer_Syntax.local_theory_to_proof "typedef" "HOL type definition (requires non-emptiness proof)"
+    Keyword.thy_goal
+    (Scan.optional (Parse.$$$ "(" |--
+        ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
+          Parse.binding >> (fn s => (true, SOME s))) --| Parse.$$$ ")") (true, NONE) --
+      (Parse.type_args_constrained -- Parse.binding) --
+        Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.term) --
+        Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding))
     >> (fn ((((((def, opt_name), (args, t)), mx), A), morphs)) =>
         typedef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs)));
 
 end;
 
-end;
-
diff -r f5417836dbea -r 01594f816e3a src/HOLCF/IOA/meta_theory/automaton.ML
--- a/src/HOLCF/IOA/meta_theory/automaton.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/automaton.ML	Mon May 17 23:54:15 2010 +0200
@@ -485,52 +485,50 @@
 
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterKeyword in
-
-val _ = List.app OuterKeyword.keyword ["signature", "actions", "inputs",
+val _ = List.app Keyword.keyword ["signature", "actions", "inputs",
   "outputs", "internals", "states", "initially", "transitions", "pre",
   "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
   "rename"];
 
-val actionlist = P.list1 P.term;
-val inputslist = P.$$$ "inputs" |-- P.!!! actionlist;
-val outputslist = P.$$$ "outputs" |-- P.!!! actionlist;
-val internalslist = P.$$$ "internals" |-- P.!!! actionlist;
-val stateslist = P.$$$ "states" |-- P.!!! (Scan.repeat1 (P.name --| P.$$$ "::" -- P.typ));
-val initial = P.$$$ "initially" |-- P.!!! P.term;
-val assign_list = P.list1 (P.name --| P.$$$ ":=" -- P.!!! P.term);
-val pre = P.$$$ "pre" |-- P.!!! P.term;
-val post = P.$$$ "post" |-- P.!!! assign_list;
+val actionlist = Parse.list1 Parse.term;
+val inputslist = Parse.$$$ "inputs" |-- Parse.!!! actionlist;
+val outputslist = Parse.$$$ "outputs" |-- Parse.!!! actionlist;
+val internalslist = Parse.$$$ "internals" |-- Parse.!!! actionlist;
+val stateslist =
+  Parse.$$$ "states" |-- Parse.!!! (Scan.repeat1 (Parse.name --| Parse.$$$ "::" -- Parse.typ));
+val initial = Parse.$$$ "initially" |-- Parse.!!! Parse.term;
+val assign_list = Parse.list1 (Parse.name --| Parse.$$$ ":=" -- Parse.!!! Parse.term);
+val pre = Parse.$$$ "pre" |-- Parse.!!! Parse.term;
+val post = Parse.$$$ "post" |-- Parse.!!! assign_list;
 val pre1 = (pre -- (Scan.optional post [])) >> mk_trans_of_prepost;
 val post1 = ((Scan.optional pre "True") -- post) >> mk_trans_of_prepost;
-val transrel =  (P.$$$ "transrel" |-- P.!!! P.term) >> mk_trans_of_rel;
-val transition = P.term -- (transrel || pre1 || post1);
-val translist = P.$$$ "transitions" |-- P.!!! (Scan.repeat1 transition);
+val transrel =  (Parse.$$$ "transrel" |-- Parse.!!! Parse.term) >> mk_trans_of_rel;
+val transition = Parse.term -- (transrel || pre1 || post1);
+val translist = Parse.$$$ "transitions" |-- Parse.!!! (Scan.repeat1 transition);
 
 val ioa_decl =
-  (P.name -- (P.$$$ "=" |--
-    (P.$$$ "signature" |--
-      P.!!! (P.$$$ "actions" |--
-        (P.typ --
+  (Parse.name -- (Parse.$$$ "=" |--
+    (Parse.$$$ "signature" |--
+      Parse.!!! (Parse.$$$ "actions" |--
+        (Parse.typ --
           (Scan.optional inputslist []) --
           (Scan.optional outputslist []) --
           (Scan.optional internalslist []) --
           stateslist --
           (Scan.optional initial "True") --
         translist))))) >> mk_ioa_decl ||
-  (P.name -- (P.$$$ "=" |-- (P.$$$ "compose" |-- P.!!! (P.list1 P.name))))
+  (Parse.name -- (Parse.$$$ "=" |-- (Parse.$$$ "compose" |-- Parse.!!! (Parse.list1 Parse.name))))
     >> mk_composition_decl ||
-  (P.name -- (P.$$$ "=" |-- (P.$$$ "hide_action" |--
-      P.!!! (P.list1 P.term -- (P.$$$ "in" |-- P.name))))) >> mk_hiding_decl ||
-  (P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |--
-      P.!!! (P.name -- (P.$$$ "to" |-- P.list1 P.term))))) >> mk_restriction_decl ||
-  (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- (P.!!! (P.name -- (P.$$$ "to" |-- P.term))))))
+  (Parse.name -- (Parse.$$$ "=" |-- (Parse.$$$ "hide_action" |--
+      Parse.!!! (Parse.list1 Parse.term -- (Parse.$$$ "in" |-- Parse.name))))) >> mk_hiding_decl ||
+  (Parse.name -- (Parse.$$$ "=" |-- (Parse.$$$ "restrict" |--
+      Parse.!!! (Parse.name -- (Parse.$$$ "to" |-- Parse.list1 Parse.term))))) >> mk_restriction_decl ||
+  (Parse.name -- (Parse.$$$ "=" |--
+      (Parse.$$$ "rename" |-- (Parse.!!! (Parse.name -- (Parse.$$$ "to" |-- Parse.term))))))
     >> mk_rename_decl;
 
 val _ =
-  OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" K.thy_decl
+  Outer_Syntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" Keyword.thy_decl
     (ioa_decl >> Toplevel.theory);
 
 end;
-
-end;
diff -r f5417836dbea -r 01594f816e3a src/HOLCF/Tools/Domain/domain_extender.ML
--- a/src/HOLCF/Tools/Domain/domain_extender.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Mon May 17 23:54:15 2010 +0200
@@ -224,27 +224,25 @@
 
 (** outer syntax **)
 
-local structure P = OuterParse and K = OuterKeyword in
-
-val _ = OuterKeyword.keyword "lazy";
+val _ = Keyword.keyword "lazy";
 
 val dest_decl : (bool * binding option * string) parser =
-  P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
-    (P.binding >> SOME) -- (P.$$$ "::" |-- P.typ)  --| P.$$$ ")" >> P.triple1
-    || P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")"
+  Parse.$$$ "(" |-- Scan.optional (Parse.$$$ "lazy" >> K true) false --
+    (Parse.binding >> SOME) -- (Parse.$$$ "::" |-- Parse.typ)  --| Parse.$$$ ")" >> Parse.triple1
+    || Parse.$$$ "(" |-- Parse.$$$ "lazy" |-- Parse.typ --| Parse.$$$ ")"
     >> (fn t => (true,NONE,t))
-    || P.typ >> (fn t => (false,NONE,t));
+    || Parse.typ >> (fn t => (false,NONE,t));
 
 val cons_decl =
-  P.binding -- Scan.repeat dest_decl -- P.opt_mixfix;
+  Parse.binding -- Scan.repeat dest_decl -- Parse.opt_mixfix;
 
 val domain_decl =
-  (P.type_args_constrained -- P.binding -- P.opt_mixfix) --
-    (P.$$$ "=" |-- P.enum1 "|" cons_decl);
+  (Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix) --
+    (Parse.$$$ "=" |-- Parse.enum1 "|" cons_decl);
 
 val domains_decl =
-  Scan.option (P.$$$ "(" |-- P.binding --| P.$$$ ")") --
-    P.and_list1 domain_decl;
+  Scan.option (Parse.$$$ "(" |-- Parse.binding --| Parse.$$$ ")") --
+    Parse.and_list1 domain_decl;
 
 fun mk_domain
     (definitional : bool)
@@ -267,13 +265,11 @@
   end;
 
 val _ =
-  OuterSyntax.command "domain" "define recursive domains (HOLCF)"
-    K.thy_decl (domains_decl >> (Toplevel.theory o mk_domain false));
+  Outer_Syntax.command "domain" "define recursive domains (HOLCF)"
+    Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain false));
 
 val _ =
-  OuterSyntax.command "new_domain" "define recursive domains (HOLCF)"
-    K.thy_decl (domains_decl >> (Toplevel.theory o mk_domain true));
+  Outer_Syntax.command "new_domain" "define recursive domains (HOLCF)"
+    Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain true));
 
 end;
-
-end;
diff -r f5417836dbea -r 01594f816e3a src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon May 17 23:54:15 2010 +0200
@@ -707,21 +707,20 @@
 
 local
 
-structure P = OuterParse and K = OuterKeyword
-
 val parse_domain_iso :
     (string list * binding * mixfix * string * (binding * binding) option)
       parser =
-  (P.type_args -- P.binding -- P.opt_mixfix -- (P.$$$ "=" |-- P.typ) --
-    Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding)))
+  (Parse.type_args -- Parse.binding -- Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) --
+    Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding)))
     >> (fn ((((vs, t), mx), rhs), morphs) => (vs, t, mx, rhs, morphs));
 
-val parse_domain_isos = P.and_list1 parse_domain_iso;
+val parse_domain_isos = Parse.and_list1 parse_domain_iso;
 
 in
 
 val _ =
-  OuterSyntax.command "domain_isomorphism" "define domain isomorphisms (HOLCF)" K.thy_decl
+  Outer_Syntax.command "domain_isomorphism" "define domain isomorphisms (HOLCF)"
+    Keyword.thy_decl
     (parse_domain_isos >> (Toplevel.theory o domain_isomorphism_cmd));
 
 end;
diff -r f5417836dbea -r 01594f816e3a src/HOLCF/Tools/cont_consts.ML
--- a/src/HOLCF/Tools/cont_consts.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOLCF/Tools/cont_consts.ML	Mon May 17 23:54:15 2010 +0200
@@ -93,12 +93,8 @@
 
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterKeyword in
-
 val _ =
-  OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl
-    (Scan.repeat1 P.const_binding >> (Toplevel.theory o add_consts_cmd));
+  Outer_Syntax.command "consts" "declare constants (HOLCF)" Keyword.thy_decl
+    (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o add_consts_cmd));
 
 end;
-
-end;
diff -r f5417836dbea -r 01594f816e3a src/HOLCF/Tools/fixrec.ML
--- a/src/HOLCF/Tools/fixrec.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOLCF/Tools/fixrec.ML	Mon May 17 23:54:15 2010 +0200
@@ -443,16 +443,14 @@
 (******************************** Parsers ********************************)
 (*************************************************************************)
 
-local structure P = OuterParse and K = OuterKeyword in
+val _ =
+  Outer_Syntax.local_theory "fixrec" "define recursive functions (HOLCF)" Keyword.thy_decl
+    ((Parse.opt_keyword "permissive" >> not) -- Parse.fixes -- Parse_Spec.where_alt_specs
+      >> (fn ((strict, fixes), specs) => add_fixrec_cmd strict fixes specs));
 
-val _ = OuterSyntax.local_theory "fixrec" "define recursive functions (HOLCF)" K.thy_decl
-  ((P.opt_keyword "permissive" >> not) -- P.fixes -- Parse_Spec.where_alt_specs
-    >> (fn ((strict, fixes), specs) => add_fixrec_cmd strict fixes specs));
-
-val _ = OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl
-  (Parse_Spec.specs >> (Toplevel.theory o add_fixpat_cmd));
-
-end;
+val _ =
+  Outer_Syntax.command "fixpat" "define rewrites for fixrec functions" Keyword.thy_decl
+    (Parse_Spec.specs >> (Toplevel.theory o add_fixpat_cmd));
 
 val setup =
   Attrib.setup @{binding fixrec_simp}
diff -r f5417836dbea -r 01594f816e3a src/HOLCF/Tools/pcpodef.ML
--- a/src/HOLCF/Tools/pcpodef.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOLCF/Tools/pcpodef.ML	Mon May 17 23:54:15 2010 +0200
@@ -355,29 +355,29 @@
 
 (** outer syntax **)
 
-local structure P = OuterParse and K = OuterKeyword in
-
 val typedef_proof_decl =
-  Scan.optional (P.$$$ "(" |--
-      ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
-        --| P.$$$ ")") (true, NONE) --
-    (P.type_args_constrained -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) --
-    Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
+  Scan.optional (Parse.$$$ "(" |--
+      ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
+        Parse.binding >> (fn s => (true, SOME s)))
+        --| Parse.$$$ ")") (true, NONE) --
+    (Parse.type_args_constrained -- Parse.binding) -- Parse.opt_mixfix --
+    (Parse.$$$ "=" |-- Parse.term) --
+    Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding));
 
 fun mk_pcpodef_proof pcpo ((((((def, opt_name), (args, t)), mx), A), morphs)) =
   (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
     ((def, the_default t opt_name), (t, args, mx), A, morphs);
 
 val _ =
-  OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
+  Outer_Syntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)"
+  Keyword.thy_goal
     (typedef_proof_decl >>
       (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)));
 
 val _ =
-  OuterSyntax.command "cpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
+  Outer_Syntax.command "cpodef" "HOLCF type definition (requires admissibility proof)"
+  Keyword.thy_goal
     (typedef_proof_decl >>
       (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)));
 
 end;
-
-end;
diff -r f5417836dbea -r 01594f816e3a src/HOLCF/Tools/repdef.ML
--- a/src/HOLCF/Tools/repdef.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/HOLCF/Tools/repdef.ML	Mon May 17 23:54:15 2010 +0200
@@ -168,23 +168,21 @@
 
 (** outer syntax **)
 
-local structure P = OuterParse and K = OuterKeyword in
-
 val repdef_decl =
-  Scan.optional (P.$$$ "(" |--
-      ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
-        --| P.$$$ ")") (true, NONE) --
-    (P.type_args_constrained -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) --
-    Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
+  Scan.optional (Parse.$$$ "(" |--
+      ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
+        Parse.binding >> (fn s => (true, SOME s)))
+        --| Parse.$$$ ")") (true, NONE) --
+    (Parse.type_args_constrained -- Parse.binding) --
+    Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.term) --
+    Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding));
 
 fun mk_repdef ((((((def, opt_name), (args, t)), mx), A), morphs)) =
   repdef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs);
 
 val _ =
-  OuterSyntax.command "repdef" "HOLCF definition of representable domains" K.thy_decl
+  Outer_Syntax.command "repdef" "HOLCF definition of representable domains" Keyword.thy_decl
     (repdef_decl >>
       (Toplevel.print oo (Toplevel.theory o mk_repdef)));
 
 end;
-
-end;
diff -r f5417836dbea -r 01594f816e3a src/Provers/blast.ML
--- a/src/Provers/blast.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/Provers/blast.ML	Mon May 17 23:54:15 2010 +0200
@@ -1309,7 +1309,7 @@
 val setup =
   setup_depth_limit #>
   Method.setup @{binding blast}
-    (Scan.lift (Scan.option OuterParse.nat) --| Method.sections Data.cla_modifiers >>
+    (Scan.lift (Scan.option Parse.nat) --| Method.sections Data.cla_modifiers >>
       (fn NONE => Data.cla_meth' blast_tac
         | SOME lim => Data.cla_meth' (fn cs => depth_tac cs lim)))
     "classical tableau prover";
diff -r f5417836dbea -r 01594f816e3a src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/Provers/clasimp.ML	Mon May 17 23:54:15 2010 +0200
@@ -275,7 +275,7 @@
   Method.sections clasimp_modifiers >> K (clasimp_meth' tac);
 
 val auto_method =
-  Scan.lift (Scan.option (OuterParse.nat -- OuterParse.nat)) --|
+  Scan.lift (Scan.option (Parse.nat -- Parse.nat)) --|
     Method.sections clasimp_modifiers >>
   (fn NONE => clasimp_meth (CHANGED_PROP o auto_tac)
     | SOME (m, n) => clasimp_meth (CHANGED_PROP o (fn css => mk_auto_tac css m n)));
diff -r f5417836dbea -r 01594f816e3a src/Provers/classical.ML
--- a/src/Provers/classical.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/Provers/classical.ML	Mon May 17 23:54:15 2010 +0200
@@ -1015,8 +1015,8 @@
 (** outer syntax **)
 
 val _ =
-  OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner"
-    OuterKeyword.diag
+  Outer_Syntax.improper_command "print_claset" "print context of Classical Reasoner"
+    Keyword.diag
     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
       Toplevel.keep (print_cs o claset_of o Toplevel.context_of)));
 
diff -r f5417836dbea -r 01594f816e3a src/Tools/Code/code_eval.ML
--- a/src/Tools/Code/code_eval.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/Code/code_eval.ML	Mon May 17 23:54:15 2010 +0200
@@ -204,26 +204,24 @@
 
 local
 
-structure P = OuterParse
-and K = OuterKeyword
-
 val datatypesK = "datatypes";
 val functionsK = "functions";
 val fileK = "file";
 val andK = "and"
 
-val _ = List.app K.keyword [datatypesK, functionsK];
+val _ = List.app Keyword.keyword [datatypesK, functionsK];
 
-val parse_datatype = (P.name --| P.$$$ "=" -- (P.term ::: (Scan.repeat (P.$$$ "|" |-- P.term))));
+val parse_datatype =
+  Parse.name --| Parse.$$$ "=" -- (Parse.term ::: (Scan.repeat (Parse.$$$ "|" |-- Parse.term)));
 
 in
 
 val _ =
-  OuterSyntax.command "code_reflect" "enrich runtime environment with generated code"
-    K.thy_decl (P.name -- Scan.optional (P.$$$ datatypesK |-- (parse_datatype
-      ::: Scan.repeat (P.$$$ andK |-- parse_datatype))) []
-    -- Scan.optional (P.$$$ functionsK |-- Scan.repeat1 P.name) []
-    -- Scan.option (P.$$$ fileK |-- P.name)
+  Outer_Syntax.command "code_reflect" "enrich runtime environment with generated code"
+    Keyword.thy_decl (Parse.name -- Scan.optional (Parse.$$$ datatypesK |-- (parse_datatype
+      ::: Scan.repeat (Parse.$$$ andK |-- parse_datatype))) []
+    -- Scan.optional (Parse.$$$ functionsK |-- Scan.repeat1 Parse.name) []
+    -- Scan.option (Parse.$$$ fileK |-- Parse.name)
   >> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory
     (code_reflect_cmd raw_datatypes raw_functions module_name some_file)));
 
diff -r f5417836dbea -r 01594f816e3a src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML	Mon May 17 23:54:15 2010 +0200
@@ -469,8 +469,8 @@
       serialize_haskell module_prefix module_name string_classes));
 
 val _ =
-  OuterSyntax.command "code_monad" "define code syntax for monads" OuterKeyword.thy_decl (
-    OuterParse.term_group -- OuterParse.name >> (fn (raw_bind, target) =>
+  Outer_Syntax.command "code_monad" "define code syntax for monads" Keyword.thy_decl (
+    Parse.term_group -- Parse.name >> (fn (raw_bind, target) =>
       Toplevel.theory  (add_monad target raw_bind))
   );
 
diff -r f5417836dbea -r 01594f816e3a src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML	Mon May 17 23:54:15 2010 +0200
@@ -479,8 +479,8 @@
   end;
 
 val _ =
-  OuterSyntax.improper_command "print_codeproc" "print code preprocessor setup"
-  OuterKeyword.diag (Scan.succeed
+  Outer_Syntax.improper_command "print_codeproc" "print code preprocessor setup"
+  Keyword.diag (Scan.succeed
       (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
         (print_codeproc o Toplevel.theory_of)));
 
diff -r f5417836dbea -r 01594f816e3a src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/Code/code_printer.ML	Mon May 17 23:54:15 2010 +0200
@@ -329,15 +329,15 @@
 
 fun parse_syntax prep_arg xs =
   Scan.option ((
-      ((OuterParse.$$$ infixK >> K X)
-        || (OuterParse.$$$ infixlK >> K L)
-        || (OuterParse.$$$ infixrK >> K R))
-        -- OuterParse.nat >> parse_infix prep_arg
+      ((Parse.$$$ infixK >> K X)
+        || (Parse.$$$ infixlK >> K L)
+        || (Parse.$$$ infixrK >> K R))
+        -- Parse.nat >> parse_infix prep_arg
       || Scan.succeed (parse_mixfix prep_arg))
-      -- OuterParse.string
+      -- Parse.string
       >> (fn (parse, s) => parse s)) xs;
 
-val _ = List.app OuterKeyword.keyword [infixK, infixlK, infixrK];
+val _ = List.app Keyword.keyword [infixK, infixlK, infixrK];
 
 
 (** module name spaces **)
diff -r f5417836dbea -r 01594f816e3a src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Mon May 17 23:54:15 2010 +0200
@@ -463,9 +463,6 @@
 
 local
 
-structure P = OuterParse
-and K = OuterKeyword
-
 fun zip_list (x::xs) f g =
   f
   #-> (fn y =>
@@ -473,9 +470,9 @@
     #-> (fn xys => pair ((x, y) :: xys)));
 
 fun parse_multi_syntax parse_thing parse_syntax =
-  P.and_list1 parse_thing
-  #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name --
-        (zip_list things parse_syntax (P.$$$ "and")) --| P.$$$ ")"));
+  Parse.and_list1 parse_thing
+  #-> (fn things => Scan.repeat1 (Parse.$$$ "(" |-- Parse.name --
+        (zip_list things parse_syntax (Parse.$$$ "and")) --| Parse.$$$ ")"));
 
 in
 
@@ -507,75 +504,79 @@
 val (inK, module_nameK, fileK) = ("in", "module_name", "file");
 
 val code_exprP =
-  (Scan.repeat1 P.term_group
-  -- Scan.repeat (P.$$$ inK |-- P.name
-     -- Scan.option (P.$$$ module_nameK |-- P.name)
-     -- Scan.option (P.$$$ fileK |-- P.name)
-     -- Scan.optional (P.$$$ "(" |-- Args.parse --| P.$$$ ")") []
+  (Scan.repeat1 Parse.term_group
+  -- Scan.repeat (Parse.$$$ inK |-- Parse.name
+     -- Scan.option (Parse.$$$ module_nameK |-- Parse.name)
+     -- Scan.option (Parse.$$$ fileK |-- Parse.name)
+     -- Scan.optional (Parse.$$$ "(" |-- Args.parse --| Parse.$$$ ")") []
   ) >> (fn (raw_cs, seris) => export_code_cmd raw_cs seris));
 
-val _ = List.app OuterKeyword.keyword [inK, module_nameK, fileK];
+val _ = List.app Keyword.keyword [inK, module_nameK, fileK];
 
 val _ =
-  OuterSyntax.command "code_class" "define code syntax for class" K.thy_decl (
-    parse_multi_syntax P.xname (Scan.option P.string)
+  Outer_Syntax.command "code_class" "define code syntax for class" Keyword.thy_decl (
+    parse_multi_syntax Parse.xname (Scan.option Parse.string)
     >> (Toplevel.theory oo fold) (fn (target, syns) =>
           fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)
   );
 
 val _ =
-  OuterSyntax.command "code_instance" "define code syntax for instance" K.thy_decl (
-    parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname) (Scan.option (P.minus >> K ()))
+  Outer_Syntax.command "code_instance" "define code syntax for instance" Keyword.thy_decl (
+    parse_multi_syntax (Parse.xname --| Parse.$$$ "::" -- Parse.xname)
+      (Scan.option (Parse.minus >> K ()))
     >> (Toplevel.theory oo fold) (fn (target, syns) =>
           fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns)
   );
 
 val _ =
-  OuterSyntax.command "code_type" "define code syntax for type constructor" K.thy_decl (
-    parse_multi_syntax P.xname (Code_Printer.parse_syntax I)
+  Outer_Syntax.command "code_type" "define code syntax for type constructor" Keyword.thy_decl (
+    parse_multi_syntax Parse.xname (Code_Printer.parse_syntax I)
     >> (Toplevel.theory oo fold) (fn (target, syns) =>
           fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns)
   );
 
 val _ =
-  OuterSyntax.command "code_const" "define code syntax for constant" K.thy_decl (
-    parse_multi_syntax P.term_group (Code_Printer.parse_syntax fst)
+  Outer_Syntax.command "code_const" "define code syntax for constant" Keyword.thy_decl (
+    parse_multi_syntax Parse.term_group (Code_Printer.parse_syntax fst)
     >> (Toplevel.theory oo fold) (fn (target, syns) =>
       fold (fn (raw_const, syn) => add_syntax_const_simple_cmd target raw_const syn) syns)
   );
 
 val _ =
-  OuterSyntax.command "code_reserved" "declare words as reserved for target language" K.thy_decl (
-    P.name -- Scan.repeat1 P.name
+  Outer_Syntax.command "code_reserved" "declare words as reserved for target language"
+    Keyword.thy_decl (
+    Parse.name -- Scan.repeat1 Parse.name
     >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds)
   );
 
 val _ =
-  OuterSyntax.command "code_include" "declare piece of code to be included in generated code" K.thy_decl (
-    P.name -- P.name -- (P.text :|-- (fn "-" => Scan.succeed NONE
-      | s => Scan.optional (P.$$$ "attach" |-- Scan.repeat1 P.term) [] >> pair s >> SOME))
+  Outer_Syntax.command "code_include" "declare piece of code to be included in generated code"
+    Keyword.thy_decl (
+    Parse.name -- Parse.name -- (Parse.text :|-- (fn "-" => Scan.succeed NONE
+      | s => Scan.optional (Parse.$$$ "attach" |-- Scan.repeat1 Parse.term) [] >> pair s >> SOME))
     >> (fn ((target, name), content_consts) =>
         (Toplevel.theory o add_include_cmd target) (name, content_consts))
   );
 
 val _ =
-  OuterSyntax.command "code_modulename" "alias module to other name" K.thy_decl (
-    P.name -- Scan.repeat1 (P.name -- P.name)
+  Outer_Syntax.command "code_modulename" "alias module to other name" Keyword.thy_decl (
+    Parse.name -- Scan.repeat1 (Parse.name -- Parse.name)
     >> (fn (target, modlnames) => (Toplevel.theory o fold (add_module_alias target)) modlnames)
   );
 
 val _ =
-  OuterSyntax.command "code_abort" "permit constant to be implemented as program abort" K.thy_decl (
-    Scan.repeat1 P.term_group >> (Toplevel.theory o fold allow_abort_cmd)
+  Outer_Syntax.command "code_abort" "permit constant to be implemented as program abort"
+    Keyword.thy_decl (
+    Scan.repeat1 Parse.term_group >> (Toplevel.theory o fold allow_abort_cmd)
   );
 
 val _ =
-  OuterSyntax.command "export_code" "generate executable code for constants"
-    K.diag (P.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
+  Outer_Syntax.command "export_code" "generate executable code for constants"
+    Keyword.diag (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
 
 fun shell_command thyname cmd = Toplevel.program (fn _ =>
-  (use_thy thyname; case Scan.read Token.stopper (P.!!! code_exprP)
-    ((filter Token.is_proper o OuterSyntax.scan Position.none) cmd)
+  (use_thy thyname; case Scan.read Token.stopper (Parse.!!! code_exprP)
+    ((filter Token.is_proper o Outer_Syntax.scan Position.none) cmd)
    of SOME f => (writeln "Now generating code..."; f (theory thyname))
     | NONE => error ("Bad directive " ^ quote cmd)))
   handle Runtime.TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
diff -r f5417836dbea -r 01594f816e3a src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML	Mon May 17 23:54:15 2010 +0200
@@ -915,23 +915,21 @@
 
 local
 
-structure P = OuterParse
-and K = OuterKeyword
-
 fun code_thms_cmd thy = code_thms thy o op @ o read_const_exprs thy;
 fun code_deps_cmd thy = code_deps thy o op @ o read_const_exprs thy;
 
 in
 
 val _ =
-  OuterSyntax.improper_command "code_thms" "print system of code equations for code" OuterKeyword.diag
-    (Scan.repeat1 P.term_group
+  Outer_Syntax.improper_command "code_thms" "print system of code equations for code" Keyword.diag
+    (Scan.repeat1 Parse.term_group
       >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
         o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
 
 val _ =
-  OuterSyntax.improper_command "code_deps" "visualize dependencies of code equations for code" OuterKeyword.diag
-    (Scan.repeat1 P.term_group
+  Outer_Syntax.improper_command "code_deps" "visualize dependencies of code equations for code"
+    Keyword.diag
+    (Scan.repeat1 Parse.term_group
       >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
         o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
 
diff -r f5417836dbea -r 01594f816e3a src/Tools/WWW_Find/find_theorems.ML
--- a/src/Tools/WWW_Find/find_theorems.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/WWW_Find/find_theorems.ML	Mon May 17 23:54:15 2010 +0200
@@ -158,21 +158,17 @@
 
 end;
 
-structure P = OuterParse
-      and K = OuterKeyword
-      and FT = Find_Theorems;
-
 val criterion =
-  P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Find_Theorems.Name ||
-  P.reserved "intro" >> K Find_Theorems.Intro ||
-  P.reserved "elim" >> K Find_Theorems.Elim ||
-  P.reserved "dest" >> K Find_Theorems.Dest ||
-  P.reserved "solves" >> K Find_Theorems.Solves ||
-  P.reserved "simp" |-- P.!!! (P.$$$ ":" |-- P.term) >> Find_Theorems.Simp ||
-  P.term >> Find_Theorems.Pattern;
+  Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Find_Theorems.Name ||
+  Parse.reserved "intro" >> K Find_Theorems.Intro ||
+  Parse.reserved "elim" >> K Find_Theorems.Elim ||
+  Parse.reserved "dest" >> K Find_Theorems.Dest ||
+  Parse.reserved "solves" >> K Find_Theorems.Solves ||
+  Parse.reserved "simp" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.term) >> Find_Theorems.Simp ||
+  Parse.term >> Find_Theorems.Pattern;
 
 val parse_query =
-  Scan.repeat (((Scan.option P.minus >> is_none) -- criterion));
+  Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion));
 
 fun app_index f xs = fold_index (fn x => K (f x)) xs ();
 
@@ -194,7 +190,7 @@
     fun get_query () =
       query
       |> (fn s => s ^ ";")
-      |> OuterSyntax.scan Position.start
+      |> Outer_Syntax.scan Position.start
       |> filter Token.is_proper
       |> Scan.error parse_query
       |> fst;
diff -r f5417836dbea -r 01594f816e3a src/Tools/WWW_Find/unicode_symbols.ML
--- a/src/Tools/WWW_Find/unicode_symbols.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/WWW_Find/unicode_symbols.ML	Mon May 17 23:54:15 2010 +0200
@@ -114,8 +114,6 @@
 
 local (* Parser *)
 
-structure P = OuterParse;
-
 fun $$$ kw = Scan.one (is_keyword kw) >> str_of_token;
 val hex_code = Scan.one is_hex_code >> int_of_code;
 val ascii_sym = Scan.one is_ascii_sym >> str_of_token;
@@ -129,7 +127,7 @@
 
 in
 
-val line = (symbol -- unicode --| font -- abbr) >> P.triple1;
+val line = (symbol -- unicode --| font -- abbr) >> Parse.triple1;
 
 val symbols_path =
   [getenv "ISABELLE_HOME", "etc", "symbols"]
diff -r f5417836dbea -r 01594f816e3a src/Tools/eqsubst.ML
--- a/src/Tools/eqsubst.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/eqsubst.ML	Mon May 17 23:54:15 2010 +0200
@@ -556,7 +556,7 @@
      (Scan.succeed false);
 
 val ith_syntax =
-    Scan.optional (Args.parens (Scan.repeat OuterParse.nat)) [0];
+    Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0];
 
 (* combination method that takes a flag (true indicates that subst
    should be done to an assumption, false = apply to the conclusion of
diff -r f5417836dbea -r 01594f816e3a src/Tools/induct.ML
--- a/src/Tools/induct.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/induct.ML	Mon May 17 23:54:15 2010 +0200
@@ -254,8 +254,8 @@
   end;
 
 val _ =
-  OuterSyntax.improper_command "print_induct_rules" "print induction and cases rules"
-    OuterKeyword.diag (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+  Outer_Syntax.improper_command "print_induct_rules" "print induction and cases rules"
+    Keyword.diag (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
       Toplevel.keep (print_rules o Toplevel.context_of)));
 
 
@@ -845,8 +845,6 @@
 
 (** concrete syntax **)
 
-structure P = OuterParse;
-
 val arbitraryN = "arbitrary";
 val takingN = "taking";
 val ruleN = "rule";
@@ -892,7 +890,7 @@
     Args.$$$ predN || Args.$$$ setN || Args.$$$ ruleN) -- Args.colon)) scan;
 
 val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |--
-  P.and_list1' (Scan.repeat (unless_more_args free))) [];
+  Parse.and_list1' (Scan.repeat (unless_more_args free))) [];
 
 val taking = Scan.optional (Scan.lift (Args.$$$ takingN -- Args.colon) |--
   Scan.repeat1 (unless_more_args inst)) [];
@@ -902,7 +900,7 @@
 val cases_setup =
   Method.setup @{binding cases}
     (Args.mode no_simpN --
-      (P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
+      (Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
       (fn (no_simp, (insts, opt_rule)) => fn ctxt =>
         METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL
           (cases_tac ctxt (not no_simp) insts opt_rule facts)))))
@@ -910,11 +908,12 @@
 
 val induct_setup =
   Method.setup @{binding induct}
-    (Args.mode no_simpN -- (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
+    (Args.mode no_simpN -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
       (arbitrary -- taking -- Scan.option induct_rule)) >>
       (fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn ctxt =>
         RAW_METHOD_CASES (fn facts =>
-          Seq.DETERM (HEADGOAL (induct_tac ctxt (not no_simp) insts arbitrary taking opt_rule facts)))))
+          Seq.DETERM
+            (HEADGOAL (induct_tac ctxt (not no_simp) insts arbitrary taking opt_rule facts)))))
     "induction on types or predicates/sets";
 
 val coinduct_setup =
diff -r f5417836dbea -r 01594f816e3a src/Tools/induct_tacs.ML
--- a/src/Tools/induct_tacs.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/induct_tacs.ML	Mon May 17 23:54:15 2010 +0200
@@ -116,8 +116,7 @@
 val opt_rules = Scan.option (rule_spec |-- Attrib.thms);
 
 val varss =
-  OuterParse.and_list'
-    (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_source))));
+  Parse.and_list' (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_source))));
 
 in
 
diff -r f5417836dbea -r 01594f816e3a src/Tools/intuitionistic.ML
--- a/src/Tools/intuitionistic.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/intuitionistic.ML	Mon May 17 23:54:15 2010 +0200
@@ -71,7 +71,7 @@
 val destN = "dest";
 
 fun modifier name kind kind' att =
-  Args.$$$ name |-- (kind >> K NONE || kind' |-- OuterParse.nat --| Args.colon >> SOME)
+  Args.$$$ name |-- (kind >> K NONE || kind' |-- Parse.nat --| Args.colon >> SOME)
     >> (pair (I: Proof.context -> Proof.context) o att);
 
 val modifiers =
@@ -87,7 +87,7 @@
 
 fun method_setup name =
   Method.setup name
-    (Scan.lift (Scan.option OuterParse.nat) --| Method.sections modifiers >>
+    (Scan.lift (Scan.option Parse.nat) --| Method.sections modifiers >>
       (fn opt_lim => fn ctxt =>
         SIMPLE_METHOD' (Object_Logic.atomize_prems_tac THEN' prover_tac ctxt opt_lim)))
     "intuitionistic proof search";
diff -r f5417836dbea -r 01594f816e3a src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/nbe.ML	Mon May 17 23:54:15 2010 +0200
@@ -625,15 +625,12 @@
 
 val setup = Value.add_evaluator ("nbe", norm o ProofContext.theory_of);
 
-local structure P = OuterParse and K = OuterKeyword in
-
-val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
+val opt_modes =
+  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
 
 val _ =
-  OuterSyntax.improper_command "normal_form" "normalize term by evaluation" K.diag
-    (opt_modes -- P.term >> (Toplevel.keep o norm_print_term_cmd));
-
-end;
+  Outer_Syntax.improper_command "normal_form" "normalize term by evaluation" Keyword.diag
+    (opt_modes -- Parse.term >> (Toplevel.keep o norm_print_term_cmd));
 
 end;
  
\ No newline at end of file
diff -r f5417836dbea -r 01594f816e3a src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/quickcheck.ML	Mon May 17 23:54:15 2010 +0200
@@ -315,27 +315,25 @@
     test_goal quiet report generator_name size iterations default_type no_assms insts i assms state
   end;
 
-fun quickcheck args i state = fst (gen_quickcheck args i state)
+fun quickcheck args i state = fst (gen_quickcheck args i state);
 
 fun quickcheck_cmd args i state =
   gen_quickcheck args i (Toplevel.proof_of state)
   |> Pretty.writeln o pretty_counterex_and_reports (Toplevel.context_of state);
 
-local structure P = OuterParse and K = OuterKeyword in
+val parse_arg = Parse.name -- (Scan.optional (Parse.$$$ "=" |-- Parse.name) "true");
 
-val parse_arg = P.name -- (Scan.optional (P.$$$ "=" |-- P.name) "true")
-
-val parse_args = P.$$$ "[" |-- P.list1 parse_arg --| P.$$$ "]"
+val parse_args = Parse.$$$ "[" |-- Parse.list1 parse_arg --| Parse.$$$ "]"
   || Scan.succeed [];
 
-val _ = OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl
-  (parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args)));
+val _ =
+  Outer_Syntax.command "quickcheck_params" "set parameters for random testing" Keyword.thy_decl
+    (parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args)));
 
-val _ = OuterSyntax.improper_command "quickcheck" "try to find counterexample for subgoal" K.diag
-  (parse_args -- Scan.optional P.nat 1
-    >> (fn (args, i) => Toplevel.no_timing o Toplevel.keep (quickcheck_cmd args i)));
-
-end; (*local*)
+val _ =
+  Outer_Syntax.improper_command "quickcheck" "try to find counterexample for subgoal" Keyword.diag
+    (parse_args -- Scan.optional Parse.nat 1
+      >> (fn (args, i) => Toplevel.no_timing o Toplevel.keep (quickcheck_cmd args i)));
 
 end;
 
diff -r f5417836dbea -r 01594f816e3a src/Tools/value.ML
--- a/src/Tools/value.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/value.ML	Mon May 17 23:54:15 2010 +0200
@@ -52,15 +52,13 @@
         Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
   in Pretty.writeln p end;
 
-local structure P = OuterParse and K = OuterKeyword in
-
-val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
+val opt_modes =
+  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
 
-val _ = OuterSyntax.improper_command "value" "evaluate and print term" K.diag
-  (Scan.option (P.$$$ "[" |-- P.xname --| P.$$$ "]") -- opt_modes -- P.term
-    >> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep
-        (value_cmd some_name modes t)));
-
-end; (*local*)
+val _ =
+  Outer_Syntax.improper_command "value" "evaluate and print term" Keyword.diag
+    (Scan.option (Parse.$$$ "[" |-- Parse.xname --| Parse.$$$ "]") -- opt_modes -- Parse.term
+      >> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep
+          (value_cmd some_name modes t)));
 
 end;
diff -r f5417836dbea -r 01594f816e3a src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Mon May 17 23:54:15 2010 +0200
@@ -419,29 +419,26 @@
 
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterKeyword in
-
 fun mk_datatype ((((dom, dts), monos), type_intrs), type_elims) =
   #1 o add_datatype (dom, map fst dts) (map snd dts) (monos, type_intrs, type_elims);
 
 val con_decl =
-  P.name -- Scan.optional (P.$$$ "(" |-- P.list1 P.term --| P.$$$ ")") [] -- P.opt_mixfix
-  >> P.triple1;
+  Parse.name -- Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.term --| Parse.$$$ ")") [] --
+    Parse.opt_mixfix >> Parse.triple1;
 
 val datatype_decl =
-  (Scan.optional ((P.$$$ "\<subseteq>" || P.$$$ "<=") |-- P.!!! P.term) "") --
-  P.and_list1 (P.term -- (P.$$$ "=" |-- P.enum1 "|" con_decl)) --
-  Scan.optional (P.$$$ "monos" |-- P.!!! Parse_Spec.xthms1) [] --
-  Scan.optional (P.$$$ "type_intros" |-- P.!!! Parse_Spec.xthms1) [] --
-  Scan.optional (P.$$$ "type_elims" |-- P.!!! Parse_Spec.xthms1) []
+  (Scan.optional ((Parse.$$$ "\<subseteq>" || Parse.$$$ "<=") |-- Parse.!!! Parse.term) "") --
+  Parse.and_list1 (Parse.term -- (Parse.$$$ "=" |-- Parse.enum1 "|" con_decl)) --
+  Scan.optional (Parse.$$$ "monos" |-- Parse.!!! Parse_Spec.xthms1) [] --
+  Scan.optional (Parse.$$$ "type_intros" |-- Parse.!!! Parse_Spec.xthms1) [] --
+  Scan.optional (Parse.$$$ "type_elims" |-- Parse.!!! Parse_Spec.xthms1) []
   >> (Toplevel.theory o mk_datatype);
 
 val coind_prefix = if coind then "co" else "";
 
-val _ = OuterSyntax.command (coind_prefix ^ "datatype")
-  ("define " ^ coind_prefix ^ "datatype") K.thy_decl datatype_decl;
+val _ =
+  Outer_Syntax.command (coind_prefix ^ "datatype")
+    ("define " ^ coind_prefix ^ "datatype") Keyword.thy_decl datatype_decl;
 
 end;
 
-end;
-
diff -r f5417836dbea -r 01594f816e3a src/ZF/Tools/ind_cases.ML
--- a/src/ZF/Tools/ind_cases.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/ZF/Tools/ind_cases.ML	Mon May 17 23:54:15 2010 +0200
@@ -64,15 +64,11 @@
 
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterKeyword in
-
 val _ =
-  OuterSyntax.command "inductive_cases"
-    "create simplified instances of elimination rules (improper)" K.thy_script
-    (P.and_list1 (Parse_Spec.opt_thm_name ":" -- Scan.repeat1 P.prop)
+  Outer_Syntax.command "inductive_cases"
+    "create simplified instances of elimination rules (improper)" Keyword.thy_script
+    (Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Scan.repeat1 Parse.prop)
       >> (Toplevel.theory o inductive_cases));
 
 end;
 
-end;
-
diff -r f5417836dbea -r 01594f816e3a src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Mon May 17 23:54:15 2010 +0200
@@ -186,25 +186,20 @@
 
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterKeyword in
-
-val _ = List.app OuterKeyword.keyword ["elimination", "induction", "case_eqns", "recursor_eqns"];
+val _ = List.app Keyword.keyword ["elimination", "induction", "case_eqns", "recursor_eqns"];
 
 val rep_datatype_decl =
-  (P.$$$ "elimination" |-- P.!!! Parse_Spec.xthm) --
-  (P.$$$ "induction" |-- P.!!! Parse_Spec.xthm) --
-  (P.$$$ "case_eqns" |-- P.!!! Parse_Spec.xthms1) --
-  Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! Parse_Spec.xthms1) []
+  (Parse.$$$ "elimination" |-- Parse.!!! Parse_Spec.xthm) --
+  (Parse.$$$ "induction" |-- Parse.!!! Parse_Spec.xthm) --
+  (Parse.$$$ "case_eqns" |-- Parse.!!! Parse_Spec.xthms1) --
+  Scan.optional (Parse.$$$ "recursor_eqns" |-- Parse.!!! Parse_Spec.xthms1) []
   >> (fn (((x, y), z), w) => rep_datatype x y z w);
 
 val _ =
-  OuterSyntax.command "rep_datatype" "represent existing set inductively" K.thy_decl
+  Outer_Syntax.command "rep_datatype" "represent existing set inductively" Keyword.thy_decl
     (rep_datatype_decl >> Toplevel.theory);
 
 end;
 
-end;
-
-
 val exhaust_tac = DatatypeTactics.exhaust_tac;
 val induct_tac  = DatatypeTactics.induct_tac;
diff -r f5417836dbea -r 01594f816e3a src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Mon May 17 23:54:15 2010 +0200
@@ -576,29 +576,26 @@
 
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterKeyword in
-
-val _ = List.app OuterKeyword.keyword
+val _ = List.app Keyword.keyword
   ["domains", "intros", "monos", "con_defs", "type_intros", "type_elims"];
 
 fun mk_ind (((((doms, intrs), monos), con_defs), type_intrs), type_elims) =
-  #1 o add_inductive doms (map P.triple_swap intrs) (monos, con_defs, type_intrs, type_elims);
+  #1 o add_inductive doms (map Parse.triple_swap intrs) (monos, con_defs, type_intrs, type_elims);
 
 val ind_decl =
-  (P.$$$ "domains" |-- P.!!! (P.enum1 "+" P.term --
-      ((P.$$$ "\<subseteq>" || P.$$$ "<=") |-- P.term))) --
-  (P.$$$ "intros" |--
-    P.!!! (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- P.prop))) --
-  Scan.optional (P.$$$ "monos" |-- P.!!! Parse_Spec.xthms1) [] --
-  Scan.optional (P.$$$ "con_defs" |-- P.!!! Parse_Spec.xthms1) [] --
-  Scan.optional (P.$$$ "type_intros" |-- P.!!! Parse_Spec.xthms1) [] --
-  Scan.optional (P.$$$ "type_elims" |-- P.!!! Parse_Spec.xthms1) []
+  (Parse.$$$ "domains" |-- Parse.!!! (Parse.enum1 "+" Parse.term --
+      ((Parse.$$$ "\<subseteq>" || Parse.$$$ "<=") |-- Parse.term))) --
+  (Parse.$$$ "intros" |--
+    Parse.!!! (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop))) --
+  Scan.optional (Parse.$$$ "monos" |-- Parse.!!! Parse_Spec.xthms1) [] --
+  Scan.optional (Parse.$$$ "con_defs" |-- Parse.!!! Parse_Spec.xthms1) [] --
+  Scan.optional (Parse.$$$ "type_intros" |-- Parse.!!! Parse_Spec.xthms1) [] --
+  Scan.optional (Parse.$$$ "type_elims" |-- Parse.!!! Parse_Spec.xthms1) []
   >> (Toplevel.theory o mk_ind);
 
-val _ = OuterSyntax.command (co_prefix ^ "inductive")
-  ("define " ^ co_prefix ^ "inductive sets") K.thy_decl ind_decl;
+val _ =
+  Outer_Syntax.command (co_prefix ^ "inductive")
+    ("define " ^ co_prefix ^ "inductive sets") Keyword.thy_decl ind_decl;
 
 end;
 
-end;
-
diff -r f5417836dbea -r 01594f816e3a src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/ZF/Tools/primrec_package.ML	Mon May 17 23:54:15 2010 +0200
@@ -194,12 +194,11 @@
 
 (* outer syntax *)
 
-structure P = OuterParse and K = OuterKeyword;
-
 val _ =
-  OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
-    (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- P.prop)
-      >> (Toplevel.theory o (#1 oo (add_primrec o map P.triple_swap))));
+  Outer_Syntax.command "primrec" "define primitive recursive functions on datatypes"
+    Keyword.thy_decl
+    (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)
+      >> (Toplevel.theory o (#1 oo (add_primrec o map Parse.triple_swap))));
 
 end;
 
diff -r f5417836dbea -r 01594f816e3a src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/ZF/Tools/typechk.ML	Mon May 17 23:54:15 2010 +0200
@@ -118,7 +118,7 @@
     "ZF type-checking";
 
 val _ =
-  OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag
+  Outer_Syntax.improper_command "print_tcset" "print context of ZF typecheck" Keyword.diag
     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
       Toplevel.keep (print_tcset o Toplevel.context_of)));