# HG changeset patch
# User huffman
# Date 1274189322 25200
# Node ID 4ec5131c6f4604737928be82f4186b55e49b5a66
# Parent  71c8973a604b7c65100a98eec0a21b83b0670368# Parent  b0033a307d1fcd410cd5b4515871d8d0fb9638a5
merged

diff -r 71c8973a604b -r 4ec5131c6f46 NEWS
--- a/NEWS	Mon May 17 18:59:59 2010 -0700
+++ b/NEWS	Tue May 18 06:28:42 2010 -0700
@@ -506,14 +506,18 @@
 context actually works, but under normal circumstances one needs to
 pass the proper local context through the code!
 
-* Renamed some important ML structures, while keeping the old names as
-legacy aliases for some time:
-
+* Renamed some important ML structures, while keeping the old names
+for some time as aliases within the structure Legacy:
+
+  OuterKeyword  ~>  Keyword
+  OuterLex      ~>  Token
+  OuterParse    ~>  Parse
   OuterSyntax   ~>  Outer_Syntax
-  OuterKeyword  ~>  Keyword
-  OuterParse    ~>  Parse
   SpecParse     ~>  Parse_Spec
 
+Note that "open Legacy" simplifies porting of sources, but forgetting
+to remove it again will complicate porting again in the future.
+
 
 *** System ***
 
diff -r 71c8973a604b -r 4ec5131c6f46 doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Mon May 17 18:59:59 2010 -0700
+++ b/doc-src/antiquote_setup.ML	Tue May 18 06:28:42 2010 -0700
@@ -166,9 +166,9 @@
 in
 
 val _ = entity_antiqs no_check "" "syntax";
-val _ = entity_antiqs (K (is_some o OuterKeyword.command_keyword)) "isacommand" "command";
-val _ = entity_antiqs (K OuterKeyword.is_keyword) "isakeyword" "keyword";
-val _ = entity_antiqs (K OuterKeyword.is_keyword) "isakeyword" "element";
+val _ = entity_antiqs (K (is_some o Keyword.command_keyword)) "isacommand" "command";
+val _ = entity_antiqs (K Keyword.is_keyword) "isakeyword" "keyword";
+val _ = entity_antiqs (K Keyword.is_keyword) "isakeyword" "element";
 val _ = entity_antiqs (thy_check Method.intern Method.defined) "" "method";
 val _ = entity_antiqs (thy_check Attrib.intern Attrib.defined) "" "attribute";
 val _ = entity_antiqs no_check "" "fact";
diff -r 71c8973a604b -r 4ec5131c6f46 doc-src/rail.ML
--- a/doc-src/rail.ML	Mon May 17 18:59:59 2010 -0700
+++ b/doc-src/rail.ML	Tue May 18 06:28:42 2010 -0700
@@ -59,9 +59,9 @@
 (*  [(kind, (markup, check, style))*)
   Symtab.make [
   ("syntax", ("", no_check, true)),
-  ("command", ("isacommand", K (is_some o OuterKeyword.command_keyword), true)),
-  ("keyword", ("isakeyword", K OuterKeyword.is_keyword, true)),
-  ("element", ("isakeyword", K OuterKeyword.is_keyword, true)),
+  ("command", ("isacommand", K (is_some o Keyword.command_keyword), true)),
+  ("keyword", ("isakeyword", K Keyword.is_keyword, true)),
+  ("element", ("isakeyword", K Keyword.is_keyword, true)),
   ("method", ("", thy_check Method.intern Method.defined, true)),
   ("attribute", ("", thy_check Attrib.intern Attrib.defined, true)),
   ("fact", ("", no_check, true)),
@@ -473,7 +473,7 @@
   |> parse
   |> print;
 
-val _ = ThyOutput.antiquotation "rail" (Scan.lift ( OuterParse.position Args.name ))
+val _ = ThyOutput.antiquotation "rail" (Scan.lift (Parse.position Args.name))
   (fn {context = ctxt,...} => fn txt => process txt ctxt);
 
 end;
diff -r 71c8973a604b -r 4ec5131c6f46 src/FOL/ex/Iff_Oracle.thy
--- a/src/FOL/ex/Iff_Oracle.thy	Mon May 17 18:59:59 2010 -0700
+++ b/src/FOL/ex/Iff_Oracle.thy	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Boogie/Tools/boogie_commands.ML
--- a/src/HOL/Boogie/Tools/boogie_commands.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Decision_Procs/Approximation.thy	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Import/import_syntax.ML
--- a/src/HOL/Import/import_syntax.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Import/import_syntax.ML	Tue May 18 06:28:42 2010 -0700
@@ -4,26 +4,23 @@
 
 signature HOL4_IMPORT_SYNTAX =
 sig
-    type token = OuterLex.token
-    type command  = token list -> (theory -> theory) * token list 
-
-    val import_segment: token list -> (theory -> theory) * token list
-    val import_theory : token list -> (theory -> theory) * token list
-    val end_import    : token list -> (theory -> theory) * token list
-
-    val setup_theory  : token list -> (theory -> theory) * token list
-    val end_setup     : token list -> (theory -> theory) * token list
+    val import_segment: (theory -> theory) parser
+    val import_theory : (theory -> theory) parser
+    val end_import    : (theory -> theory) parser
+                        
+    val setup_theory  : (theory -> theory) parser
+    val end_setup     : (theory -> theory) parser
+                        
+    val thm_maps      : (theory -> theory) parser
+    val ignore_thms   : (theory -> theory) parser
+    val type_maps     : (theory -> theory) parser
+    val def_maps      : (theory -> theory) parser
+    val const_maps    : (theory -> theory) parser
+    val const_moves   : (theory -> theory) parser
+    val const_renames : (theory -> theory) parser
 
-    val thm_maps      : token list -> (theory -> theory) * token list
-    val ignore_thms   : token list -> (theory -> theory) * token list
-    val type_maps     : token list -> (theory -> theory) * token list
-    val def_maps      : token list -> (theory -> theory) * token list
-    val const_maps    : token list -> (theory -> theory) * token list
-    val const_moves   : token list -> (theory -> theory) * token list
-    val const_renames : token list -> (theory -> theory) * token list
-
-    val skip_import_dir : token list -> (theory -> theory) * token list
-    val skip_import     : token list -> (theory -> theory) * token list
+    val skip_import_dir : (theory -> theory) parser
+    val skip_import     : (theory -> theory) parser
 
     val setup        : unit -> unit
 end
@@ -31,28 +28,23 @@
 structure HOL4ImportSyntax :> HOL4_IMPORT_SYNTAX =
 struct
 
-type token = OuterLex.token
-type command  = token list -> (theory -> theory) * token list 
-
-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 : command = 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 : command = P.short_ident >> do_skip_import
+val skip_import = Parse.short_ident >> do_skip_import
 
 fun end_import toks =
     Scan.succeed
@@ -84,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
@@ -93,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
@@ -102,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
@@ -111,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
@@ -120,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
@@ -129,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
@@ -139,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
@@ -160,18 +152,18 @@
           (Scan.make_lexicon (map Symbol.explode ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"]),
                   Scan.empty_lexicon)
         val get_lexes = fn () => !lexes
-        val token_source = OuterLex.source {do_recover = NONE} get_lexes Position.start symb_source
-        val token_list = filter_out (OuterLex.is_kind OuterLex.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 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 = 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
@@ -194,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 =>
@@ -218,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 71c8973a604b -r 4ec5131c6f46 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Import/proof_kernel.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML
--- a/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue May 18 06:28:42 2010 -0700
@@ -330,14 +330,14 @@
 
 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
     |> Symbol.source {do_recover=false}
-    |> OuterLex.source {do_recover=SOME false} lex Position.start
-    |> OuterLex.source_proper
-    |> Source.source OuterLex.stopper (Parse_Spec.xthms1 >> get) NONE
+    |> Token.source {do_recover=SOME false} lex Position.start
+    |> Token.source_proper
+    |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
     |> Source.exhaust
   end
 
diff -r 71c8973a604b -r 4ec5131c6f46 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Nominal/nominal_atoms.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Nominal/nominal_datatype.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Nominal/nominal_induct.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Nominal/nominal_inductive.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Nominal/nominal_primrec.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Orderings.thy	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Statespace/state_space.ML	Tue May 18 06:28:42 2010 -0700
@@ -32,10 +32,9 @@
        (string * typ) list -> theory -> theory
 
     val statespace_decl :
-       OuterParse.token list ->
        ((string list * bstring) *
          ((string list * xstring * (bstring * bstring) list) list *
-          (bstring * string) list)) * OuterParse.token list
+          (bstring * string) list)) parser
 
 
     val neq_x_y : Proof.context -> term -> term -> thm option
@@ -668,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 71c8973a604b -r 4ec5131c6f46 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/Datatype/datatype.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Tools/Datatype/datatype_data.ML
--- a/src/HOL/Tools/Datatype/datatype_data.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Tools/Function/fun.ML
--- a/src/HOL/Tools/Function/fun.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/Function/fun.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/Function/function.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/Function/function_common.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Tools/Quotient/quotient_info.ML
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Tools/Quotient/quotient_typ.ML
--- a/src/HOL/Tools/Quotient/quotient_typ.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/choice_specification.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/inductive.ML	Tue May 18 06:28:42 2010 -0700
@@ -83,8 +83,7 @@
     (binding * string option * mixfix) list ->
     (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
     bool -> local_theory -> inductive_result * local_theory
-  val gen_ind_decl: add_ind_def -> bool ->
-    OuterParse.token list -> (bool -> local_theory -> local_theory) * OuterParse.token list
+  val gen_ind_decl: add_ind_def -> bool -> (bool -> local_theory -> local_theory) parser
 end;
 
 structure Inductive: INDUCTIVE =
@@ -971,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 71c8973a604b -r 4ec5131c6f46 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/inductive_codegen.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/inductive_set.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/primrec.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/recdef.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/record.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Tools/refute_isar.ML
--- a/src/HOL/Tools/refute_isar.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/refute_isar.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Tools/split_rule.ML
--- a/src/HOL/Tools/split_rule.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/split_rule.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/typedef.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOLCF/IOA/meta_theory/automaton.ML
--- a/src/HOLCF/IOA/meta_theory/automaton.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOLCF/IOA/meta_theory/automaton.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOLCF/Tools/Domain/domain_extender.ML
--- a/src/HOLCF/Tools/Domain/domain_extender.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOLCF/Tools/cont_consts.ML
--- a/src/HOLCF/Tools/cont_consts.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOLCF/Tools/cont_consts.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOLCF/Tools/fixrec.ML
--- a/src/HOLCF/Tools/fixrec.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOLCF/Tools/fixrec.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOLCF/Tools/pcpodef.ML
--- a/src/HOLCF/Tools/pcpodef.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOLCF/Tools/pcpodef.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/HOLCF/Tools/repdef.ML
--- a/src/HOLCF/Tools/repdef.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/HOLCF/Tools/repdef.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Provers/blast.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Provers/clasimp.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Provers/classical.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/General/scan.scala	Tue May 18 06:28:42 2010 -0700
@@ -258,47 +258,44 @@
 
     /* outer syntax tokens */
 
-    def token(symbols: Symbol.Interpretation, is_command: String => Boolean):
-      Parser[Outer_Lex.Token] =
+    def token(symbols: Symbol.Interpretation, is_command: String => Boolean): Parser[Token] =
     {
-      import Outer_Lex.Token_Kind, Outer_Lex.Token
-
       val id = one(symbols.is_letter) ~ many(symbols.is_letdig) ^^ { case x ~ y => x + y }
       val nat = many1(symbols.is_digit)
       val id_nat = id ~ opt("." ~ nat) ^^ { case x ~ Some(y ~ z) => x + y + z case x ~ None => x }
 
       val ident = id ~ rep("." ~> id) ^^
-        { case x ~ Nil => Token(Token_Kind.IDENT, x)
-          case x ~ ys => Token(Token_Kind.LONG_IDENT, (x :: ys).mkString(".")) }
+        { case x ~ Nil => Token(Token.Kind.IDENT, x)
+          case x ~ ys => Token(Token.Kind.LONG_IDENT, (x :: ys).mkString(".")) }
 
-      val var_ = "?" ~ id_nat ^^ { case x ~ y => Token(Token_Kind.VAR, x + y) }
-      val type_ident = "'" ~ id ^^ { case x ~ y => Token(Token_Kind.TYPE_IDENT, x + y) }
-      val type_var = "?'" ~ id_nat ^^ { case x ~ y => Token(Token_Kind.TYPE_VAR, x + y) }
-      val nat_ = nat ^^ (x => Token(Token_Kind.NAT, x))
+      val var_ = "?" ~ id_nat ^^ { case x ~ y => Token(Token.Kind.VAR, x + y) }
+      val type_ident = "'" ~ id ^^ { case x ~ y => Token(Token.Kind.TYPE_IDENT, x + y) }
+      val type_var = "?'" ~ id_nat ^^ { case x ~ y => Token(Token.Kind.TYPE_VAR, x + y) }
+      val nat_ = nat ^^ (x => Token(Token.Kind.NAT, x))
 
       val sym_ident =
         (many1(symbols.is_symbolic_char) |
           one(sym => symbols.is_symbolic(sym) & Symbol.is_wellformed(sym))) ^^
-        (x => Token(Token_Kind.SYM_IDENT, x))
+        (x => Token(Token.Kind.SYM_IDENT, x))
 
-      val space = many1(symbols.is_blank) ^^ (x => Token(Token_Kind.SPACE, x))
+      val space = many1(symbols.is_blank) ^^ (x => Token(Token.Kind.SPACE, x))
 
-      val string = quoted("\"") ^^ (x => Token(Token_Kind.STRING, x))
-      val alt_string = quoted("`") ^^ (x => Token(Token_Kind.ALT_STRING, x))
+      val string = quoted("\"") ^^ (x => Token(Token.Kind.STRING, x))
+      val alt_string = quoted("`") ^^ (x => Token(Token.Kind.ALT_STRING, x))
 
       val junk = many1(sym => !(symbols.is_blank(sym)))
       val bad_delimiter =
-        ("\"" | "`" | "{*" | "(*") ~ junk ^^ { case x ~ y => Token(Token_Kind.BAD_INPUT, x + y) }
-      val bad = junk ^^ (x => Token(Token_Kind.BAD_INPUT, x))
+        ("\"" | "`" | "{*" | "(*") ~ junk ^^ { case x ~ y => Token(Token.Kind.BAD_INPUT, x + y) }
+      val bad = junk ^^ (x => Token(Token.Kind.BAD_INPUT, x))
 
 
       /* tokens */
 
-      (space | (string | (alt_string | (verbatim ^^ (x => Token(Token_Kind.VERBATIM, x)) |
-        comment ^^ (x => Token(Token_Kind.COMMENT, x)))))) |
+      (space | (string | (alt_string | (verbatim ^^ (x => Token(Token.Kind.VERBATIM, x)) |
+        comment ^^ (x => Token(Token.Kind.COMMENT, x)))))) |
       bad_delimiter |
       ((ident | (var_ | (type_ident | (type_var | (nat_ | sym_ident))))) |||
-        keyword ^^ (x => Token(if (is_command(x)) Token_Kind.COMMAND else Token_Kind.KEYWORD, x))) |
+        keyword ^^ (x => Token(if (is_command(x)) Token.Kind.COMMAND else Token.Kind.KEYWORD, x))) |
       bad
     }
   }
diff -r 71c8973a604b -r 4ec5131c6f46 src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/General/symbol_pos.ML	Tue May 18 06:28:42 2010 -0700
@@ -4,17 +4,12 @@
 Symbols with explicit position information.
 *)
 
-signature BASIC_SYMBOL_POS =
+signature SYMBOL_POS =
 sig
   type T = Symbol.symbol * Position.T
   val symbol: T -> Symbol.symbol
   val $$$ : Symbol.symbol -> T list -> T list * T list
   val ~$$$ : Symbol.symbol -> T list -> T list * T list
-end
-
-signature SYMBOL_POS =
-sig
-  include BASIC_SYMBOL_POS
   val content: T list -> string
   val untabify_content: T list -> string
   val is_eof: T -> bool
@@ -185,5 +180,10 @@
 
 end;
 
-structure Basic_Symbol_Pos: BASIC_SYMBOL_POS = Symbol_Pos;   (*not open by default*)
+structure Basic_Symbol_Pos =   (*not open by default*)
+struct
+  val symbol = Symbol_Pos.symbol;
+  val $$$ = Symbol_Pos.$$$;
+  val ~$$$ = Symbol_Pos.~$$$;
+end;
 
diff -r 71c8973a604b -r 4ec5131c6f46 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/IsaMakefile	Tue May 18 06:28:42 2010 -0700
@@ -67,24 +67,25 @@
   Isar/expression.ML Isar/isar_cmd.ML Isar/isar_document.ML		\
   Isar/isar_syn.ML Isar/keyword.ML Isar/local_defs.ML			\
   Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML		\
-  Isar/method.ML Isar/object_logic.ML Isar/obtain.ML Isar/outer_lex.ML	\
+  Isar/method.ML Isar/object_logic.ML Isar/obtain.ML			\
   Isar/outer_syntax.ML Isar/overloading.ML Isar/parse.ML		\
   Isar/parse_spec.ML Isar/parse_value.ML Isar/proof.ML			\
   Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML	\
   Isar/rule_cases.ML Isar/rule_insts.ML Isar/runtime.ML			\
   Isar/skip_proof.ML Isar/spec_rules.ML Isar/specification.ML		\
-  Isar/theory_target.ML Isar/toplevel.ML Isar/typedecl.ML		\
-  ML/ml_antiquote.ML ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML	\
-  ML/ml_context.ML ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML		\
-  ML/ml_syntax.ML ML/ml_thms.ML ML-Systems/install_pp_polyml.ML		\
-  ML-Systems/install_pp_polyml-5.3.ML ML-Systems/use_context.ML		\
-  Proof/extraction.ML Proof/proof_rewrite_rules.ML			\
-  Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML	\
-  ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML			\
-  ProofGeneral/pgip_isabelle.ML ProofGeneral/pgip_markup.ML		\
-  ProofGeneral/pgip_output.ML ProofGeneral/pgip_parser.ML		\
-  ProofGeneral/pgip_tests.ML ProofGeneral/pgip_types.ML			\
-  ProofGeneral/preferences.ML ProofGeneral/proof_general_emacs.ML	\
+  Isar/theory_target.ML Isar/token.ML Isar/toplevel.ML			\
+  Isar/typedecl.ML ML/ml_antiquote.ML ML/ml_compiler.ML			\
+  ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML ML/ml_env.ML		\
+  ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML ML/ml_thms.ML		\
+  ML-Systems/install_pp_polyml.ML ML-Systems/install_pp_polyml-5.3.ML	\
+  ML-Systems/use_context.ML Proof/extraction.ML				\
+  Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML			\
+  Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/pgip.ML	\
+  ProofGeneral/pgip_input.ML ProofGeneral/pgip_isabelle.ML		\
+  ProofGeneral/pgip_markup.ML ProofGeneral/pgip_output.ML		\
+  ProofGeneral/pgip_parser.ML ProofGeneral/pgip_tests.ML		\
+  ProofGeneral/pgip_types.ML ProofGeneral/preferences.ML		\
+  ProofGeneral/proof_general_emacs.ML					\
   ProofGeneral/proof_general_pgip.ML Pure.thy ROOT.ML Syntax/ast.ML	\
   Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML			\
   Syntax/printer.ML Syntax/simple_syntax.ML Syntax/syn_ext.ML		\
diff -r 71c8973a604b -r 4ec5131c6f46 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Isar/args.ML	Tue May 18 06:28:42 2010 -0700
@@ -7,10 +7,9 @@
 
 signature ARGS =
 sig
-  type token = OuterLex.token
   type src
-  val src: (string * token list) * Position.T -> src
-  val dest_src: src -> (string * token list) * Position.T
+  val src: (string * Token.T list) * Position.T -> src
+  val dest_src: src -> (string * Token.T list) * Position.T
   val pretty_src: Proof.context -> src -> Pretty.T
   val map_name: (string -> string) -> src -> src
   val morph_values: morphism -> src -> src
@@ -57,8 +56,8 @@
   val const: bool -> string context_parser
   val const_proper: bool -> string context_parser
   val goal_spec: ((int -> tactic) -> tactic) context_parser
-  val parse: token list parser
-  val parse1: (string -> bool) -> token list parser
+  val parse: Token.T list parser
+  val parse1: (string -> bool) -> Token.T list parser
   val attribs: (string -> string) -> src list parser
   val opt_attribs: (string -> string) -> src list parser
   val thm_name: (string -> string) -> string -> (binding * src list) parser
@@ -70,15 +69,9 @@
 structure Args: ARGS =
 struct
 
-structure T = OuterLex;
-
-type token = T.token;
-
-
-
 (** datatype src **)
 
-datatype src = Src of (string * token list) * Position.T;
+datatype src = Src of (string * Token.T list) * Position.T;
 
 val src = Src;
 fun dest_src (Src src) = src;
@@ -87,12 +80,12 @@
   let
     val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
     fun prt arg =
-      (case T.get_value arg of
-        SOME (T.Text s) => Pretty.str (quote s)
-      | SOME (T.Typ T) => Syntax.pretty_typ ctxt T
-      | SOME (T.Term t) => Syntax.pretty_term ctxt t
-      | SOME (T.Fact ths) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
-      | _ => Pretty.str (T.unparse arg));
+      (case Token.get_value arg of
+        SOME (Token.Text s) => Pretty.str (quote s)
+      | SOME (Token.Typ T) => Syntax.pretty_typ ctxt T
+      | SOME (Token.Term t) => Syntax.pretty_term ctxt t
+      | SOME (Token.Fact ths) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
+      | _ => Pretty.str (Token.unparse arg));
     val (s, args) = #1 (dest_src src);
   in Pretty.block (Pretty.breaks (Pretty.str s :: map prt args)) end;
 
@@ -102,15 +95,15 @@
 
 (* values *)
 
-fun morph_values phi = map_args (T.map_value
-  (fn T.Text s => T.Text s
-    | T.Typ T => T.Typ (Morphism.typ phi T)
-    | T.Term t => T.Term (Morphism.term phi t)
-    | T.Fact ths => T.Fact (Morphism.fact phi ths)
-    | T.Attribute att => T.Attribute (Morphism.transform phi att)));
+fun morph_values phi = map_args (Token.map_value
+  (fn Token.Text s => Token.Text s
+    | Token.Typ T => Token.Typ (Morphism.typ phi T)
+    | Token.Term t => Token.Term (Morphism.term phi t)
+    | Token.Fact ths => Token.Fact (Morphism.fact phi ths)
+    | Token.Attribute att => Token.Attribute (Morphism.transform phi att)));
 
-val assignable = map_args T.assignable;
-val closure = map_args T.closure;
+val assignable = map_args Token.assignable;
+val closure = map_args Token.closure;
 
 
 
@@ -134,7 +127,7 @@
 val alt_string = token Parse.alt_string;
 val symbolic = token Parse.keyword_ident_or_symbolic;
 
-fun $$$ x = (ident >> T.content_of || Parse.keyword)
+fun $$$ x = (ident >> Token.content_of || Parse.keyword)
   :|-- (fn y => if x = y then Scan.succeed x else Scan.fail);
 
 
@@ -153,39 +146,40 @@
 fun mode s = Scan.lift (Scan.optional (parens ($$$ s) >> K true) false);
 fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
 
-val name_source = named >> T.source_of;
-val name_source_position = named >> T.source_position_of;
+val name_source = named >> Token.source_of;
+val name_source_position = named >> Token.source_position_of;
 
-val name = named >> T.content_of;
+val name = named >> Token.content_of;
 val binding = Parse.position name >> Binding.make;
-val alt_name = alt_string >> T.content_of;
-val symbol = symbolic >> T.content_of;
+val alt_name = alt_string >> Token.content_of;
+val symbol = symbolic >> Token.content_of;
 val liberal_name = symbol || name;
 
-val var = (ident >> T.content_of) :|-- (fn x =>
+val var = (ident >> Token.content_of) :|-- (fn x =>
   (case Lexicon.read_variable x of SOME v => Scan.succeed v | NONE => Scan.fail));
 
 
 (* values *)
 
 fun value dest = Scan.some (fn arg =>
-  (case T.get_value arg of SOME v => (SOME (dest v) handle Match => NONE) | NONE => NONE));
+  (case Token.get_value arg of SOME v => (SOME (dest v) handle Match => NONE) | NONE => NONE));
 
 fun evaluate mk eval arg =
-  let val x = eval arg in (T.assign (SOME (mk x)) arg; x) end;
+  let val x = eval arg in (Token.assign (SOME (mk x)) arg; x) end;
+
+val internal_text = value (fn Token.Text s => s);
+val internal_typ = value (fn Token.Typ T => T);
+val internal_term = value (fn Token.Term t => t);
+val internal_fact = value (fn Token.Fact ths => ths);
+val internal_attribute = value (fn Token.Attribute att => att);
 
-val internal_text = value (fn T.Text s => s);
-val internal_typ = value (fn T.Typ T => T);
-val internal_term = value (fn T.Term t => t);
-val internal_fact = value (fn T.Fact ths => ths);
-val internal_attribute = value (fn T.Attribute att => att);
-
-fun named_text intern = internal_text || named >> evaluate T.Text (intern o T.content_of);
-fun named_typ readT = internal_typ || named >> evaluate T.Typ (readT o T.source_of);
-fun named_term read = internal_term || named >> evaluate T.Term (read o T.source_of);
-fun named_fact get = internal_fact || named >> evaluate T.Fact (get o T.content_of) ||
-  alt_string >> evaluate T.Fact (get o T.source_of);
-fun named_attribute att = internal_attribute || named >> evaluate T.Attribute (att o T.content_of);
+fun named_text intern = internal_text || named >> evaluate Token.Text (intern o Token.content_of);
+fun named_typ readT = internal_typ || named >> evaluate Token.Typ (readT o Token.source_of);
+fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.source_of);
+fun named_fact get = internal_fact || named >> evaluate Token.Fact (get o Token.content_of) ||
+  alt_string >> evaluate Token.Fact (get o Token.source_of);
+fun named_attribute att =
+  internal_attribute || named >> evaluate Token.Attribute (att o Token.content_of);
 
 
 (* terms and types *)
@@ -243,7 +237,7 @@
       (token (Parse.$$$ l) ::: Parse.!!! (args true @@@ (token (Parse.$$$ r) >> single))) x;
   in (args, args1) end;
 
-val parse = #1 (parse_args T.ident_or_symbolic) false;
+val parse = #1 (parse_args Token.ident_or_symbolic) false;
 fun parse1 is_symid = #2 (parse_args is_symid) false;
 
 
@@ -252,7 +246,7 @@
 fun attribs intern =
   let
     val attrib_name = internal_text || (symbolic || named)
-      >> evaluate T.Text (intern o T.content_of);
+      >> evaluate Token.Text (intern o Token.content_of);
     val attrib = Parse.position (attrib_name -- Parse.!!! parse) >> src;
   in $$$ "[" |-- Parse.!!! (Parse.list attrib --| $$$ "]") end;
 
@@ -273,11 +267,11 @@
 (** syntax wrapper **)
 
 fun syntax kind scan (Src ((s, args), pos)) st =
-  (case Scan.error (Scan.finite' T.stopper (Scan.option scan)) (st, args) of
+  (case Scan.error (Scan.finite' Token.stopper (Scan.option scan)) (st, args) of
     (SOME x, (st', [])) => (x, st')
   | (_, (_, args')) =>
       error (kind ^ " " ^ quote s ^ Position.str_of pos ^ ": bad arguments\n  " ^
-        space_implode " " (map T.unparse args')));
+        space_implode " " (map Token.unparse args')));
 
 fun context_syntax kind scan src = apsnd Context.the_proof o syntax kind scan src o Context.Proof;
 
diff -r 71c8973a604b -r 4ec5131c6f46 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Isar/attrib.ML	Tue May 18 06:28:42 2010 -0700
@@ -47,9 +47,6 @@
 structure Attrib: ATTRIB =
 struct
 
-structure T = OuterLex;
-
-
 (* source and bindings *)
 
 type src = Args.src;
@@ -216,7 +213,7 @@
 
 (* internal *)
 
-fun internal att = Args.src (("Pure.attribute", [T.mk_attribute att]), Position.none);
+fun internal att = Args.src (("Pure.attribute", [Token.mk_attribute att]), Position.none);
 
 
 (* rule composition *)
diff -r 71c8973a604b -r 4ec5131c6f46 src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Isar/keyword.ML	Tue May 18 06:28:42 2010 -0700
@@ -210,7 +210,4 @@
 
 end;
 
-(*legacy alias*)
-structure OuterKeyword = Keyword;
 
-
diff -r 71c8973a604b -r 4ec5131c6f46 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Isar/method.ML	Tue May 18 06:28:42 2010 -0700
@@ -411,7 +411,7 @@
 (* outer parser *)
 
 fun is_symid_meth s =
-  s <> "|" andalso s <> "?" andalso s <> "+" andalso OuterLex.ident_or_symbolic s;
+  s <> "|" andalso s <> "?" andalso s <> "+" andalso Token.ident_or_symbolic s;
 
 local
 
diff -r 71c8973a604b -r 4ec5131c6f46 src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Mon May 17 18:59:59 2010 -0700
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,390 +0,0 @@
-(*  Title:      Pure/Isar/outer_lex.ML
-    Author:     Markus Wenzel, TU Muenchen
-
-Outer lexical syntax for Isabelle/Isar.
-*)
-
-signature OUTER_LEX =
-sig
-  datatype token_kind =
-    Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
-    Nat | String | AltString | Verbatim | Space | Comment | InternalValue |
-    Malformed | Error of string | Sync | EOF
-  datatype value =
-    Text of string | Typ of typ | Term of term | Fact of thm list |
-    Attribute of morphism -> attribute
-  type token
-  val str_of_kind: token_kind -> string
-  val position_of: token -> Position.T
-  val end_position_of: token -> Position.T
-  val pos_of: token -> string
-  val eof: token
-  val is_eof: token -> bool
-  val not_eof: token -> bool
-  val not_sync: token -> bool
-  val stopper: token Scan.stopper
-  val kind_of: token -> token_kind
-  val is_kind: token_kind -> token -> bool
-  val keyword_with: (string -> bool) -> token -> bool
-  val ident_with: (string -> bool) -> token -> bool
-  val is_proper: token -> bool
-  val is_semicolon: token -> bool
-  val is_comment: token -> bool
-  val is_begin_ignore: token -> bool
-  val is_end_ignore: token -> bool
-  val is_blank: token -> bool
-  val is_newline: token -> bool
-  val source_of: token -> string
-  val source_position_of: token -> Symbol_Pos.text * Position.T
-  val content_of: token -> string
-  val unparse: token -> string
-  val text_of: token -> string * string
-  val get_value: token -> value option
-  val map_value: (value -> value) -> token -> token
-  val mk_text: string -> token
-  val mk_typ: typ -> token
-  val mk_term: term -> token
-  val mk_fact: thm list -> token
-  val mk_attribute: (morphism -> attribute) -> token
-  val assignable: token -> token
-  val assign: value option -> token -> unit
-  val closure: token -> token
-  val ident_or_symbolic: string -> bool
-  val !!! : string -> (Symbol_Pos.T list -> 'a) -> Symbol_Pos.T list -> 'a
-  val source_proper: (token, 'a) Source.source -> (token, (token, 'a) Source.source) Source.source
-  val source': {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
-    (Symbol_Pos.T, 'a) Source.source -> (token, (Symbol_Pos.T, 'a) Source.source) Source.source
-  val source: {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
-    Position.T -> (Symbol.symbol, 'a) Source.source -> (token,
-      (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
-  val read_antiq: Scan.lexicon -> (token list -> 'a * token list) ->
-    Symbol_Pos.T list * Position.T -> 'a
-end;
-
-structure OuterLex: OUTER_LEX =
-struct
-
-(** tokens **)
-
-(* token values *)
-
-(*The value slot assigns an (optional) internal value to a token,
-  usually as a side-effect of special scanner setup (see also
-  args.ML).  Note that an assignable ref designates an intermediate
-  state of internalization -- it is NOT meant to persist.*)
-
-datatype value =
-  Text of string |
-  Typ of typ |
-  Term of term |
-  Fact of thm list |
-  Attribute of morphism -> attribute;
-
-datatype slot =
-  Slot |
-  Value of value option |
-  Assignable of value option Unsynchronized.ref;
-
-
-(* datatype token *)
-
-datatype token_kind =
-  Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
-  Nat | String | AltString | Verbatim | Space | Comment | InternalValue |
-  Malformed | Error of string | Sync | EOF;
-
-datatype token = Token of (Symbol_Pos.text * Position.range) * (token_kind * string) * slot;
-
-val str_of_kind =
- fn Command => "command"
-  | Keyword => "keyword"
-  | Ident => "identifier"
-  | LongIdent => "long identifier"
-  | SymIdent => "symbolic identifier"
-  | Var => "schematic variable"
-  | TypeIdent => "type variable"
-  | TypeVar => "schematic type variable"
-  | Nat => "number"
-  | String => "string"
-  | AltString => "back-quoted string"
-  | Verbatim => "verbatim text"
-  | Space => "white space"
-  | Comment => "comment text"
-  | InternalValue => "internal value"
-  | Malformed => "malformed symbolic character"
-  | Error _ => "bad input"
-  | Sync => "sync marker"
-  | EOF => "end-of-file";
-
-
-(* position *)
-
-fun position_of (Token ((_, (pos, _)), _, _)) = pos;
-fun end_position_of (Token ((_, (_, pos)), _, _)) = pos;
-
-val pos_of = Position.str_of o position_of;
-
-
-(* control tokens *)
-
-fun mk_eof pos = Token (("", (pos, Position.none)), (EOF, ""), Slot);
-val eof = mk_eof Position.none;
-
-fun is_eof (Token (_, (EOF, _), _)) = true
-  | is_eof _ = false;
-
-val not_eof = not o is_eof;
-
-fun not_sync (Token (_, (Sync, _), _)) = false
-  | not_sync _ = true;
-
-val stopper =
-  Scan.stopper (fn [] => eof | toks => mk_eof (end_position_of (List.last toks))) is_eof;
-
-
-(* kind of token *)
-
-fun kind_of (Token (_, (k, _), _)) = k;
-fun is_kind k (Token (_, (k', _), _)) = k = k';
-
-fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
-  | keyword_with _ _ = false;
-
-fun ident_with pred (Token (_, (Ident, x), _)) = pred x
-  | ident_with _ _ = false;
-
-fun is_proper (Token (_, (Space, _), _)) = false
-  | is_proper (Token (_, (Comment, _), _)) = false
-  | is_proper _ = true;
-
-fun is_semicolon (Token (_, (Keyword, ";"), _)) = true
-  | is_semicolon _ = false;
-
-fun is_comment (Token (_, (Comment, _), _)) = true
-  | is_comment _ = false;
-
-fun is_begin_ignore (Token (_, (Comment, "<"), _)) = true
-  | is_begin_ignore _ = false;
-
-fun is_end_ignore (Token (_, (Comment, ">"), _)) = true
-  | is_end_ignore _ = false;
-
-
-(* blanks and newlines -- space tokens obey lines *)
-
-fun is_blank (Token (_, (Space, x), _)) = not (String.isSuffix "\n" x)
-  | is_blank _ = false;
-
-fun is_newline (Token (_, (Space, x), _)) = String.isSuffix "\n" x
-  | is_newline _ = false;
-
-
-(* token content *)
-
-fun source_of (Token ((source, (pos, _)), _, _)) =
-  YXML.string_of (XML.Elem (Markup.tokenN, Position.properties_of pos, [XML.Text source]));
-
-fun source_position_of (Token ((source, (pos, _)), _, _)) = (source, pos);
-
-fun content_of (Token (_, (_, x), _)) = x;
-
-
-(* unparse *)
-
-fun escape q =
-  implode o map (fn s => if s = q orelse s = "\\" then "\\" ^ s else s) o Symbol.explode;
-
-fun unparse (Token (_, (kind, x), _)) =
-  (case kind of
-    String => x |> quote o escape "\""
-  | AltString => x |> enclose "`" "`" o escape "`"
-  | Verbatim => x |> enclose "{*" "*}"
-  | Comment => x |> enclose "(*" "*)"
-  | Malformed => space_implode " " (explode x)
-  | Sync => ""
-  | EOF => ""
-  | _ => x);
-
-fun text_of tok =
-  if is_semicolon tok then ("terminator", "")
-  else
-    let
-      val k = str_of_kind (kind_of tok);
-      val s = unparse tok
-        handle ERROR _ => Symbol.separate_chars (content_of tok);
-    in
-      if s = "" then (k, "")
-      else if size s < 40 andalso not (exists_string (fn c => c = "\n") s) then (k ^ " " ^ s, "")
-      else (k, s)
-    end;
-
-
-
-(** associated values **)
-
-(* access values *)
-
-fun get_value (Token (_, _, Value v)) = v
-  | get_value _ = NONE;
-
-fun map_value f (Token (x, y, Value (SOME v))) = Token (x, y, Value (SOME (f v)))
-  | map_value _ tok = tok;
-
-
-(* make values *)
-
-fun mk_value k v = Token ((k, Position.no_range), (InternalValue, k), Value (SOME v));
-
-val mk_text = mk_value "<text>" o Text;
-val mk_typ = mk_value "<typ>" o Typ;
-val mk_term = mk_value "<term>" o Term;
-val mk_fact = mk_value "<fact>" o Fact;
-val mk_attribute = mk_value "<attribute>" o Attribute;
-
-
-(* static binding *)
-
-(*1st stage: make empty slots assignable*)
-fun assignable (Token (x, y, Slot)) = Token (x, y, Assignable (Unsynchronized.ref NONE))
-  | assignable tok = tok;
-
-(*2nd stage: assign values as side-effect of scanning*)
-fun assign v (Token (_, _, Assignable r)) = r := v
-  | assign _ _ = ();
-
-(*3rd stage: static closure of final values*)
-fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v)
-  | closure tok = tok;
-
-
-
-(** scanners **)
-
-open Basic_Symbol_Pos;
-
-fun !!! msg = Symbol_Pos.!!! ("Outer lexical error: " ^ msg);
-
-
-(* scan symbolic idents *)
-
-val is_sym_char = member (op =) (explode "!#$%&*+-/<=>?@^_|~");
-
-val scan_symid =
-  Scan.many1 (is_sym_char o symbol) ||
-  Scan.one (Symbol.is_symbolic o symbol) >> single;
-
-fun is_symid str =
-  (case try Symbol.explode str of
-    SOME [s] => Symbol.is_symbolic s orelse is_sym_char s
-  | SOME ss => forall is_sym_char ss
-  | _ => false);
-
-fun ident_or_symbolic "begin" = false
-  | ident_or_symbolic ":" = true
-  | ident_or_symbolic "::" = true
-  | ident_or_symbolic s = Syntax.is_identifier s orelse is_symid s;
-
-
-(* scan verbatim text *)
-
-val scan_verb =
-  $$$ "*" --| Scan.ahead (~$$$ "}") ||
-  Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s) >> single;
-
-val scan_verbatim =
-  (Symbol_Pos.scan_pos --| $$$ "{" --| $$$ "*") -- !!! "missing end of verbatim text"
-    (Symbol_Pos.change_prompt
-      ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- Symbol_Pos.scan_pos)));
-
-
-(* scan space *)
-
-fun is_space s = Symbol.is_blank s andalso s <> "\n";
-
-val scan_space =
-  Scan.many1 (is_space o symbol) @@@ Scan.optional ($$$ "\n") [] ||
-  Scan.many (is_space o symbol) @@@ $$$ "\n";
-
-
-(* scan comment *)
-
-val scan_comment =
-  Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body !!! -- Symbol_Pos.scan_pos);
-
-
-(* scan malformed symbols *)
-
-val scan_malformed =
-  $$$ Symbol.malformed |--
-    Symbol_Pos.change_prompt (Scan.many (Symbol.is_regular o symbol))
-  --| Scan.option ($$$ Symbol.end_malformed);
-
-
-
-(** token sources **)
-
-fun source_proper src = src |> Source.filter is_proper;
-
-local
-
-fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2;
-
-fun token k ss =
-  Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.untabify_content ss), Slot);
-
-fun token_range k (pos1, (ss, pos2)) =
-  Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.untabify_content ss), Slot);
-
-fun scan (lex1, lex2) = !!! "bad input"
-  (Symbol_Pos.scan_string >> token_range String ||
-    Symbol_Pos.scan_alt_string >> token_range AltString ||
-    scan_verbatim >> token_range Verbatim ||
-    scan_comment >> token_range Comment ||
-    scan_space >> token Space ||
-    scan_malformed >> token Malformed ||
-    Scan.one (Symbol.is_sync o symbol) >> (token Sync o single) ||
-    (Scan.max token_leq
-      (Scan.max token_leq
-        (Scan.literal lex2 >> pair Command)
-        (Scan.literal lex1 >> pair Keyword))
-      (Syntax.scan_longid >> pair LongIdent ||
-        Syntax.scan_id >> pair Ident ||
-        Syntax.scan_var >> pair Var ||
-        Syntax.scan_tid >> pair TypeIdent ||
-        Syntax.scan_tvar >> pair TypeVar ||
-        Syntax.scan_nat >> pair Nat ||
-        scan_symid >> pair SymIdent) >> uncurry token));
-
-fun recover msg =
-  Scan.many ((Symbol.is_regular andf (not o Symbol.is_blank)) o symbol)
-  >> (single o token (Error msg));
-
-in
-
-fun source' {do_recover} get_lex =
-  Source.source Symbol_Pos.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
-    (Option.map (rpair recover) do_recover);
-
-fun source do_recover get_lex pos src =
-  Symbol_Pos.source pos src
-  |> source' do_recover get_lex;
-
-end;
-
-
-(* read_antiq *)
-
-fun read_antiq lex scan (syms, pos) =
-  let
-    fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.str_of pos ^ ":\n" ^
-      "@{" ^ Symbol_Pos.content syms ^ "}");
-
-    val res =
-      Source.of_list syms
-      |> source' {do_recover = NONE} (K (lex, Scan.empty_lexicon))
-      |> source_proper
-      |> Source.source stopper (Scan.error (Scan.bulk scan)) NONE
-      |> Source.exhaust;
-  in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;
-
-end;
diff -r 71c8973a604b -r 4ec5131c6f46 src/Pure/Isar/outer_lex.scala
--- a/src/Pure/Isar/outer_lex.scala	Mon May 17 18:59:59 2010 -0700
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,94 +0,0 @@
-/*  Title:      Pure/Isar/outer_lex.scala
-    Author:     Makarius
-
-Outer lexical syntax for Isabelle/Isar.
-*/
-
-package isabelle
-
-
-object Outer_Lex
-{
-  /* tokens */
-
-  object Token_Kind extends Enumeration
-  {
-    val COMMAND = Value("command")
-    val KEYWORD = Value("keyword")
-    val IDENT = Value("identifier")
-    val LONG_IDENT = Value("long identifier")
-    val SYM_IDENT = Value("symbolic identifier")
-    val VAR = Value("schematic variable")
-    val TYPE_IDENT = Value("type variable")
-    val TYPE_VAR = Value("schematic type variable")
-    val NAT = Value("number")
-    val STRING = Value("string")
-    val ALT_STRING = Value("back-quoted string")
-    val VERBATIM = Value("verbatim text")
-    val SPACE = Value("white space")
-    val COMMENT = Value("comment text")
-    val BAD_INPUT = Value("bad input")
-    val UNPARSED = Value("unparsed input")
-  }
-
-  sealed case class Token(val kind: Token_Kind.Value, val source: String)
-  {
-    def is_command: Boolean = kind == Token_Kind.COMMAND
-    def is_delimited: Boolean =
-      kind == Token_Kind.STRING ||
-      kind == Token_Kind.ALT_STRING ||
-      kind == Token_Kind.VERBATIM ||
-      kind == Token_Kind.COMMENT
-    def is_name: Boolean =
-      kind == Token_Kind.IDENT ||
-      kind == Token_Kind.SYM_IDENT ||
-      kind == Token_Kind.STRING ||
-      kind == Token_Kind.NAT
-    def is_xname: Boolean = is_name || kind == Token_Kind.LONG_IDENT
-    def is_text: Boolean = is_xname || kind == Token_Kind.VERBATIM
-    def is_space: Boolean = kind == Token_Kind.SPACE
-    def is_comment: Boolean = kind == Token_Kind.COMMENT
-    def is_ignored: Boolean = is_space || is_comment
-    def is_unparsed: Boolean = kind == Token_Kind.UNPARSED
-
-    def content: String =
-      if (kind == Token_Kind.STRING) Scan.Lexicon.empty.quoted_content("\"", source)
-      else if (kind == Token_Kind.ALT_STRING) Scan.Lexicon.empty.quoted_content("`", source)
-      else if (kind == Token_Kind.VERBATIM) Scan.Lexicon.empty.verbatim_content(source)
-      else if (kind == Token_Kind.COMMENT) Scan.Lexicon.empty.comment_content(source)
-      else source
-
-    def text: (String, String) =
-      if (kind == Token_Kind.COMMAND && source == ";") ("terminator", "")
-      else (kind.toString, source)
-  }
-
-
-  /* token reader */
-
-  class Line_Position(val line: Int) extends scala.util.parsing.input.Position
-  {
-    def column = 0
-    def lineContents = ""
-    override def toString = line.toString
-
-    def advance(token: Token): Line_Position =
-    {
-      var n = 0
-      for (c <- token.content if c == '\n') n += 1
-      if (n == 0) this else new Line_Position(line + n)
-    }
-  }
-
-  abstract class Reader extends scala.util.parsing.input.Reader[Token]
-
-  private class Token_Reader(tokens: List[Token], val pos: Line_Position) extends Reader
-  {
-    def first = tokens.head
-    def rest = new Token_Reader(tokens.tail, pos.advance(first))
-    def atEnd = tokens.isEmpty
-  }
-
-  def reader(tokens: List[Token]): Reader = new Token_Reader(tokens, new Line_Position(1))
-}
-
diff -r 71c8973a604b -r 4ec5131c6f46 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Isar/outer_syntax.ML	Tue May 18 06:28:42 2010 -0700
@@ -25,7 +25,7 @@
   val local_theory_to_proof: string -> string -> Keyword.T ->
     (local_theory -> Proof.state) parser -> unit
   val print_outer_syntax: unit -> unit
-  val scan: Position.T -> string -> OuterLex.token list
+  val scan: Position.T -> string -> Token.T list
   val parse: Position.T -> string -> Toplevel.transition list
   val process_file: Path.T -> theory -> theory
   type isar
@@ -37,11 +37,6 @@
 structure Outer_Syntax: OUTER_SYNTAX =
 struct
 
-structure T = OuterLex;
-type 'a parser = 'a Parse.parser;
-
-
-
 (** outer syntax **)
 
 (* command parsers *)
@@ -171,17 +166,17 @@
 fun toplevel_source term do_recover cmd src =
   let
     val no_terminator =
-      Scan.unless Parse.semicolon (Scan.one (T.not_sync andf T.not_eof));
+      Scan.unless Parse.semicolon (Scan.one (Token.not_sync andf Token.not_eof));
     fun recover int =
       (int, fn _ => Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]);
   in
     src
-    |> T.source_proper
-    |> Source.source T.stopper
+    |> Token.source_proper
+    |> Source.source Token.stopper
       (Scan.bulk (Parse.$$$ "--" -- Parse.!!! Parse.doc_source >> K NONE || Parse.not_eof >> SOME))
         (Option.map recover do_recover)
     |> Source.map_filter I
-    |> Source.source T.stopper
+    |> Source.source Token.stopper
         (Scan.bulk (fn xs => Parse.!!! (parse_command term (cmd ())) xs))
         (Option.map recover do_recover)
     |> Source.map_filter I
@@ -193,13 +188,13 @@
 fun scan pos str =
   Source.of_string str
   |> Symbol.source {do_recover = false}
-  |> T.source {do_recover = SOME false} Keyword.get_lexicons pos
+  |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
   |> Source.exhaust;
 
 fun parse pos str =
   Source.of_string str
   |> Symbol.source {do_recover = false}
-  |> T.source {do_recover = SOME false} Keyword.get_lexicons pos
+  |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
   |> toplevel_source false NONE get_command
   |> Source.exhaust;
 
@@ -222,7 +217,7 @@
 
 type isar =
   (Toplevel.transition, (Toplevel.transition option,
-    (OuterLex.token, (OuterLex.token option, (OuterLex.token, (OuterLex.token,
+    (Token.T, (Token.T option, (Token.T, (Token.T,
       (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, unit) Source.source)
   Source.source) Source.source) Source.source) Source.source)
   Source.source) Source.source) Source.source) Source.source;
@@ -230,7 +225,7 @@
 fun isar term : isar =
   Source.tty
   |> Symbol.source {do_recover = true}
-  |> T.source {do_recover = SOME true} Keyword.get_lexicons Position.none
+  |> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none
   |> toplevel_source term (SOME true) get_command;
 
 
@@ -297,6 +292,3 @@
 
 end;
 
-(*legacy alias*)
-structure OuterSyntax = Outer_Syntax;
-
diff -r 71c8973a604b -r 4ec5131c6f46 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Isar/outer_syntax.scala	Tue May 18 06:28:42 2010 -0700
@@ -39,7 +39,7 @@
 
   /* tokenize */
 
-  def scan(input: Reader[Char]): List[Outer_Lex.Token] =
+  def scan(input: Reader[Char]): List[Token] =
   {
     import lexicon._
 
@@ -49,6 +49,6 @@
     }
   }
 
-  def scan(input: CharSequence): List[Outer_Lex.Token] =
+  def scan(input: CharSequence): List[Token] =
     scan(new CharSequenceReader(input))
 }
diff -r 71c8973a604b -r 4ec5131c6f46 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Isar/parse.ML	Tue May 18 06:28:42 2010 -0700
@@ -6,17 +6,16 @@
 
 signature PARSE =
 sig
-  type token = OuterLex.token
-  type 'a parser = token list -> 'a * token list
-  type 'a context_parser = Context.generic * token list -> 'a * (Context.generic * token list)
-  val group: string -> (token list -> 'a) -> token list -> 'a
-  val !!! : (token list -> 'a) -> token list -> 'a
-  val !!!! : (token list -> 'a) -> token list -> 'a
+  type 'a parser = Token.T list -> 'a * Token.T list
+  type 'a context_parser = Context.generic * Token.T list -> 'a * (Context.generic * Token.T list)
+  val group: string -> (Token.T list -> 'a) -> Token.T list -> 'a
+  val !!! : (Token.T list -> 'a) -> Token.T list -> 'a
+  val !!!! : (Token.T list -> 'a) -> Token.T list -> 'a
   val triple1: ('a * 'b) * 'c -> 'a * 'b * 'c
   val triple2: 'a * ('b * 'c) -> 'a * 'b * 'c
   val triple_swap: ('a * 'b) * 'c -> ('a * 'c) * 'b
-  val not_eof: token parser
-  val position: (token list -> 'a * 'b) -> token list -> ('a * Position.T) * 'b
+  val not_eof: Token.T parser
+  val position: (Token.T list -> 'a * 'b) -> Token.T list -> ('a * Position.T) * 'b
   val command: string parser
   val keyword: string parser
   val short_ident: string parser
@@ -98,11 +97,8 @@
 structure Parse: PARSE =
 struct
 
-structure T = OuterLex;
-type token = T.token;
-
-type 'a parser = token list -> 'a * token list;
-type 'a context_parser = Context.generic * token list -> 'a * (Context.generic * token list);
+type 'a parser = Token.T list -> 'a * Token.T list;
+type 'a context_parser = Context.generic * Token.T list -> 'a * (Context.generic * Token.T list);
 
 
 (** error handling **)
@@ -112,9 +108,11 @@
 fun fail_with s = Scan.fail_with
   (fn [] => s ^ " expected (past end-of-file!)"
     | (tok :: _) =>
-        (case T.text_of tok of
-          (txt, "") => s ^ " expected,\nbut " ^ txt ^ T.pos_of tok ^ " was found"
-        | (txt1, txt2) => s ^ " expected,\nbut " ^ txt1 ^ T.pos_of tok ^ " was found:\n" ^ txt2));
+        (case Token.text_of tok of
+          (txt, "") =>
+            s ^ " expected,\nbut " ^ txt ^ Token.pos_of tok ^ " was found"
+        | (txt1, txt2) =>
+            s ^ " expected,\nbut " ^ txt1 ^ Token.pos_of tok ^ " was found:\n" ^ txt2));
 
 fun group s scan = scan || fail_with s;
 
@@ -124,7 +122,7 @@
 fun cut kind scan =
   let
     fun get_pos [] = " (past end-of-file!)"
-      | get_pos (tok :: _) = T.pos_of tok;
+      | get_pos (tok :: _) = Token.pos_of tok;
 
     fun err (toks, NONE) = kind ^ get_pos toks
       | err (toks, SOME msg) =
@@ -149,42 +147,42 @@
 (* tokens *)
 
 fun RESET_VALUE atom = (*required for all primitive parsers*)
-  Scan.ahead (Scan.one (K true)) -- atom >> (fn (arg, x) => (T.assign NONE arg; x));
+  Scan.ahead (Scan.one (K true)) -- atom >> (fn (arg, x) => (Token.assign NONE arg; x));
 
 
-val not_eof = RESET_VALUE (Scan.one T.not_eof);
+val not_eof = RESET_VALUE (Scan.one Token.not_eof);
 
-fun position scan = (Scan.ahead not_eof >> T.position_of) -- scan >> Library.swap;
-fun source_position atom = Scan.ahead atom |-- not_eof >> T.source_position_of;
-fun inner_syntax atom = Scan.ahead atom |-- not_eof >> T.source_of;
+fun position scan = (Scan.ahead not_eof >> Token.position_of) -- scan >> Library.swap;
+fun source_position atom = Scan.ahead atom |-- not_eof >> Token.source_position_of;
+fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.source_of;
 
 fun kind k =
-  group (T.str_of_kind k) (RESET_VALUE (Scan.one (T.is_kind k) >> T.content_of));
+  group (Token.str_of_kind k) (RESET_VALUE (Scan.one (Token.is_kind k) >> Token.content_of));
 
-val command = kind T.Command;
-val keyword = kind T.Keyword;
-val short_ident = kind T.Ident;
-val long_ident = kind T.LongIdent;
-val sym_ident = kind T.SymIdent;
-val term_var = kind T.Var;
-val type_ident = kind T.TypeIdent;
-val type_var = kind T.TypeVar;
-val number = kind T.Nat;
-val string = kind T.String;
-val alt_string = kind T.AltString;
-val verbatim = kind T.Verbatim;
-val sync = kind T.Sync;
-val eof = kind T.EOF;
+val command = kind Token.Command;
+val keyword = kind Token.Keyword;
+val short_ident = kind Token.Ident;
+val long_ident = kind Token.LongIdent;
+val sym_ident = kind Token.SymIdent;
+val term_var = kind Token.Var;
+val type_ident = kind Token.TypeIdent;
+val type_var = kind Token.TypeVar;
+val number = kind Token.Nat;
+val string = kind Token.String;
+val alt_string = kind Token.AltString;
+val verbatim = kind Token.Verbatim;
+val sync = kind Token.Sync;
+val eof = kind Token.EOF;
 
-fun keyword_with pred = RESET_VALUE (Scan.one (T.keyword_with pred) >> T.content_of);
-val keyword_ident_or_symbolic = keyword_with T.ident_or_symbolic;
+fun keyword_with pred = RESET_VALUE (Scan.one (Token.keyword_with pred) >> Token.content_of);
+val keyword_ident_or_symbolic = keyword_with Token.ident_or_symbolic;
 
 fun $$$ x =
-  group (T.str_of_kind T.Keyword ^ " " ^ quote x) (keyword_with (fn y => x = y));
+  group (Token.str_of_kind Token.Keyword ^ " " ^ quote x) (keyword_with (fn y => x = y));
 
 fun reserved x =
   group ("reserved identifier " ^ quote x)
-    (RESET_VALUE (Scan.one (T.ident_with (fn y => x = y)) >> T.content_of));
+    (RESET_VALUE (Scan.one (Token.ident_with (fn y => x = y)) >> Token.content_of));
 
 val semicolon = $$$ ";";
 
@@ -341,6 +339,3 @@
 type 'a parser = 'a Parse.parser;
 type 'a context_parser = 'a Parse.context_parser;
 
-(*legacy alias*)
-structure OuterParse = Parse;
-
diff -r 71c8973a604b -r 4ec5131c6f46 src/Pure/Isar/parse.scala
--- a/src/Pure/Isar/parse.scala	Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Isar/parse.scala	Tue May 18 06:28:42 2010 -0700
@@ -15,7 +15,7 @@
 
   trait Parser extends Parsers
   {
-    type Elem = Outer_Lex.Token
+    type Elem = Token
 
     def filter_proper = true
 
@@ -50,8 +50,8 @@
       token(s, pred) ^^ (_.content)
 
     def keyword(name: String): Parser[String] =
-      atom(Outer_Lex.Token_Kind.KEYWORD.toString + " \"" + name + "\"",
-        tok => tok.kind == Outer_Lex.Token_Kind.KEYWORD && tok.content == name)
+      atom(Token.Kind.KEYWORD.toString + " \"" + name + "\"",
+        tok => tok.kind == Token.Kind.KEYWORD && tok.content == name)
 
     def name: Parser[String] = atom("name declaration", _.is_name)
     def xname: Parser[String] = atom("name reference", _.is_xname)
@@ -62,16 +62,16 @@
 
     private def tag_name: Parser[String] =
       atom("tag name", tok =>
-          tok.kind == Outer_Lex.Token_Kind.IDENT ||
-          tok.kind == Outer_Lex.Token_Kind.STRING)
+          tok.kind == Token.Kind.IDENT ||
+          tok.kind == Token.Kind.STRING)
 
     def tags: Parser[List[String]] = rep(keyword("%") ~> tag_name)
 
 
     /* wrappers */
 
-    def parse[T](p: Parser[T], in: Outer_Lex.Reader): ParseResult[T] = p(in)
-    def parse_all[T](p: Parser[T], in: Outer_Lex.Reader): ParseResult[T] = parse(phrase(p), in)
+    def parse[T](p: Parser[T], in: Token.Reader): ParseResult[T] = p(in)
+    def parse_all[T](p: Parser[T], in: Token.Reader): ParseResult[T] = parse(phrase(p), in)
   }
 }
 
diff -r 71c8973a604b -r 4ec5131c6f46 src/Pure/Isar/parse_spec.ML
--- a/src/Pure/Isar/parse_spec.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Isar/parse_spec.ML	Tue May 18 06:28:42 2010 -0700
@@ -162,6 +162,3 @@
 
 end;
 
-(*legacy alias*)
-structure SpecParse = Parse_Spec;
-
diff -r 71c8973a604b -r 4ec5131c6f46 src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Isar/rule_insts.ML	Tue May 18 06:28:42 2010 -0700
@@ -29,9 +29,6 @@
 structure RuleInsts: RULE_INSTS =
 struct
 
-structure T = OuterLex;
-
-
 (** reading instantiations **)
 
 local
@@ -100,11 +97,11 @@
 
     val (type_insts, term_insts) = List.partition (is_tvar o fst) mixed_insts;
     val internal_insts = term_insts |> map_filter
-      (fn (xi, T.Term t) => SOME (xi, t)
-        | (_, T.Text _) => NONE
+      (fn (xi, Token.Term t) => SOME (xi, t)
+        | (_, Token.Text _) => NONE
         | (xi, _) => error_var "Term argument expected for " xi);
     val external_insts = term_insts |> map_filter
-      (fn (xi, T.Text s) => SOME (xi, s) | _ => NONE);
+      (fn (xi, Token.Text s) => SOME (xi, s) | _ => NONE);
 
 
     (* mixed type instantiations *)
@@ -114,8 +111,8 @@
         val S = the_sort tvars xi;
         val T =
           (case arg of
-            T.Text s => Syntax.read_typ ctxt s
-          | T.Typ T => T
+            Token.Text s => Syntax.read_typ ctxt s
+          | Token.Typ T => T
           | _ => error_var "Type argument expected for " xi);
       in
         if Sign.of_sort thy (T, S) then ((xi, S), T)
@@ -172,9 +169,9 @@
     val _ = (*assign internalized values*)
       mixed_insts |> List.app (fn (arg, (xi, _)) =>
         if is_tvar xi then
-          T.assign (SOME (T.Typ (the (AList.lookup (op =) type_insts xi)))) arg
+          Token.assign (SOME (Token.Typ (the (AList.lookup (op =) type_insts xi)))) arg
         else
-          T.assign (SOME (T.Term (the (AList.lookup (op =) term_insts xi)))) arg);
+          Token.assign (SOME (Token.Term (the (AList.lookup (op =) term_insts xi)))) arg);
   in
     Drule.instantiate insts thm |> Rule_Cases.save thm
   end;
@@ -197,7 +194,7 @@
 
 fun read_instantiate ctxt args thm =
   read_instantiate_mixed (ctxt |> ProofContext.set_mode ProofContext.mode_schematic)  (* FIXME !? *)
-    (map (fn (x, y) => (T.eof, (x, T.Text y))) args) thm;
+    (map (fn (x, y) => (Token.eof, (x, Token.Text y))) args) thm;
 
 fun instantiate_tac ctxt args = PRIMITIVE (read_instantiate ctxt args);
 
@@ -210,9 +207,9 @@
 local
 
 val value =
-  Args.internal_typ >> T.Typ ||
-  Args.internal_term >> T.Term ||
-  Args.name_source >> T.Text;
+  Args.internal_typ >> Token.Typ ||
+  Args.internal_term >> Token.Term ||
+  Args.name_source >> Token.Text;
 
 val inst = Args.var -- (Args.$$$ "=" |-- Scan.ahead Parse.not_eof -- value)
   >> (fn (xi, (a, v)) => (a, (xi, v)));
@@ -233,8 +230,8 @@
 local
 
 val value =
-  Args.internal_term >> T.Term ||
-  Args.name_source >> T.Text;
+  Args.internal_term >> Token.Term ||
+  Args.name_source >> Token.Text;
 
 val inst = Scan.ahead Parse.not_eof -- Args.maybe value;
 val concl = Args.$$$ "concl" -- Args.colon;
diff -r 71c8973a604b -r 4ec5131c6f46 src/Pure/Isar/token.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/token.ML	Tue May 18 06:28:42 2010 -0700
@@ -0,0 +1,389 @@
+(*  Title:      Pure/Isar/token.ML
+    Author:     Markus Wenzel, TU Muenchen
+
+Outer token syntax for Isabelle/Isar.
+*)
+
+signature TOKEN =
+sig
+  datatype kind =
+    Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
+    Nat | String | AltString | Verbatim | Space | Comment | InternalValue |
+    Malformed | Error of string | Sync | EOF
+  datatype value =
+    Text of string | Typ of typ | Term of term | Fact of thm list |
+    Attribute of morphism -> attribute
+  type T
+  val str_of_kind: kind -> string
+  val position_of: T -> Position.T
+  val end_position_of: T -> Position.T
+  val pos_of: T -> string
+  val eof: T
+  val is_eof: T -> bool
+  val not_eof: T -> bool
+  val not_sync: T -> bool
+  val stopper: T Scan.stopper
+  val kind_of: T -> kind
+  val is_kind: kind -> T -> bool
+  val keyword_with: (string -> bool) -> T -> bool
+  val ident_with: (string -> bool) -> T -> bool
+  val is_proper: T -> bool
+  val is_semicolon: T -> bool
+  val is_comment: T -> bool
+  val is_begin_ignore: T -> bool
+  val is_end_ignore: T -> bool
+  val is_blank: T -> bool
+  val is_newline: T -> bool
+  val source_of: T -> string
+  val source_position_of: T -> Symbol_Pos.text * Position.T
+  val content_of: T -> string
+  val unparse: T -> string
+  val text_of: T -> string * string
+  val get_value: T -> value option
+  val map_value: (value -> value) -> T -> T
+  val mk_text: string -> T
+  val mk_typ: typ -> T
+  val mk_term: term -> T
+  val mk_fact: thm list -> T
+  val mk_attribute: (morphism -> attribute) -> T
+  val assignable: T -> T
+  val assign: value option -> T -> unit
+  val closure: T -> T
+  val ident_or_symbolic: string -> bool
+  val !!! : string -> (Symbol_Pos.T list -> 'a) -> Symbol_Pos.T list -> 'a
+  val source_proper: (T, 'a) Source.source -> (T, (T, 'a) Source.source) Source.source
+  val source': {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
+    (Symbol_Pos.T, 'a) Source.source -> (T, (Symbol_Pos.T, 'a) Source.source) Source.source
+  val source: {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
+    Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
+      (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
+  val read_antiq: Scan.lexicon -> (T list -> 'a * T list) -> Symbol_Pos.T list * Position.T -> 'a
+end;
+
+structure Token: TOKEN =
+struct
+
+(** tokens **)
+
+(* token values *)
+
+(*The value slot assigns an (optional) internal value to a token,
+  usually as a side-effect of special scanner setup (see also
+  args.ML).  Note that an assignable ref designates an intermediate
+  state of internalization -- it is NOT meant to persist.*)
+
+datatype value =
+  Text of string |
+  Typ of typ |
+  Term of term |
+  Fact of thm list |
+  Attribute of morphism -> attribute;
+
+datatype slot =
+  Slot |
+  Value of value option |
+  Assignable of value option Unsynchronized.ref;
+
+
+(* datatype token *)
+
+datatype kind =
+  Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
+  Nat | String | AltString | Verbatim | Space | Comment | InternalValue |
+  Malformed | Error of string | Sync | EOF;
+
+datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot;
+
+val str_of_kind =
+ fn Command => "command"
+  | Keyword => "keyword"
+  | Ident => "identifier"
+  | LongIdent => "long identifier"
+  | SymIdent => "symbolic identifier"
+  | Var => "schematic variable"
+  | TypeIdent => "type variable"
+  | TypeVar => "schematic type variable"
+  | Nat => "number"
+  | String => "string"
+  | AltString => "back-quoted string"
+  | Verbatim => "verbatim text"
+  | Space => "white space"
+  | Comment => "comment text"
+  | InternalValue => "internal value"
+  | Malformed => "malformed symbolic character"
+  | Error _ => "bad input"
+  | Sync => "sync marker"
+  | EOF => "end-of-file";
+
+
+(* position *)
+
+fun position_of (Token ((_, (pos, _)), _, _)) = pos;
+fun end_position_of (Token ((_, (_, pos)), _, _)) = pos;
+
+val pos_of = Position.str_of o position_of;
+
+
+(* control tokens *)
+
+fun mk_eof pos = Token (("", (pos, Position.none)), (EOF, ""), Slot);
+val eof = mk_eof Position.none;
+
+fun is_eof (Token (_, (EOF, _), _)) = true
+  | is_eof _ = false;
+
+val not_eof = not o is_eof;
+
+fun not_sync (Token (_, (Sync, _), _)) = false
+  | not_sync _ = true;
+
+val stopper =
+  Scan.stopper (fn [] => eof | toks => mk_eof (end_position_of (List.last toks))) is_eof;
+
+
+(* kind of token *)
+
+fun kind_of (Token (_, (k, _), _)) = k;
+fun is_kind k (Token (_, (k', _), _)) = k = k';
+
+fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
+  | keyword_with _ _ = false;
+
+fun ident_with pred (Token (_, (Ident, x), _)) = pred x
+  | ident_with _ _ = false;
+
+fun is_proper (Token (_, (Space, _), _)) = false
+  | is_proper (Token (_, (Comment, _), _)) = false
+  | is_proper _ = true;
+
+fun is_semicolon (Token (_, (Keyword, ";"), _)) = true
+  | is_semicolon _ = false;
+
+fun is_comment (Token (_, (Comment, _), _)) = true
+  | is_comment _ = false;
+
+fun is_begin_ignore (Token (_, (Comment, "<"), _)) = true
+  | is_begin_ignore _ = false;
+
+fun is_end_ignore (Token (_, (Comment, ">"), _)) = true
+  | is_end_ignore _ = false;
+
+
+(* blanks and newlines -- space tokens obey lines *)
+
+fun is_blank (Token (_, (Space, x), _)) = not (String.isSuffix "\n" x)
+  | is_blank _ = false;
+
+fun is_newline (Token (_, (Space, x), _)) = String.isSuffix "\n" x
+  | is_newline _ = false;
+
+
+(* token content *)
+
+fun source_of (Token ((source, (pos, _)), _, _)) =
+  YXML.string_of (XML.Elem (Markup.tokenN, Position.properties_of pos, [XML.Text source]));
+
+fun source_position_of (Token ((source, (pos, _)), _, _)) = (source, pos);
+
+fun content_of (Token (_, (_, x), _)) = x;
+
+
+(* unparse *)
+
+fun escape q =
+  implode o map (fn s => if s = q orelse s = "\\" then "\\" ^ s else s) o Symbol.explode;
+
+fun unparse (Token (_, (kind, x), _)) =
+  (case kind of
+    String => x |> quote o escape "\""
+  | AltString => x |> enclose "`" "`" o escape "`"
+  | Verbatim => x |> enclose "{*" "*}"
+  | Comment => x |> enclose "(*" "*)"
+  | Malformed => space_implode " " (explode x)
+  | Sync => ""
+  | EOF => ""
+  | _ => x);
+
+fun text_of tok =
+  if is_semicolon tok then ("terminator", "")
+  else
+    let
+      val k = str_of_kind (kind_of tok);
+      val s = unparse tok
+        handle ERROR _ => Symbol.separate_chars (content_of tok);
+    in
+      if s = "" then (k, "")
+      else if size s < 40 andalso not (exists_string (fn c => c = "\n") s) then (k ^ " " ^ s, "")
+      else (k, s)
+    end;
+
+
+
+(** associated values **)
+
+(* access values *)
+
+fun get_value (Token (_, _, Value v)) = v
+  | get_value _ = NONE;
+
+fun map_value f (Token (x, y, Value (SOME v))) = Token (x, y, Value (SOME (f v)))
+  | map_value _ tok = tok;
+
+
+(* make values *)
+
+fun mk_value k v = Token ((k, Position.no_range), (InternalValue, k), Value (SOME v));
+
+val mk_text = mk_value "<text>" o Text;
+val mk_typ = mk_value "<typ>" o Typ;
+val mk_term = mk_value "<term>" o Term;
+val mk_fact = mk_value "<fact>" o Fact;
+val mk_attribute = mk_value "<attribute>" o Attribute;
+
+
+(* static binding *)
+
+(*1st stage: make empty slots assignable*)
+fun assignable (Token (x, y, Slot)) = Token (x, y, Assignable (Unsynchronized.ref NONE))
+  | assignable tok = tok;
+
+(*2nd stage: assign values as side-effect of scanning*)
+fun assign v (Token (_, _, Assignable r)) = r := v
+  | assign _ _ = ();
+
+(*3rd stage: static closure of final values*)
+fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v)
+  | closure tok = tok;
+
+
+
+(** scanners **)
+
+open Basic_Symbol_Pos;
+
+fun !!! msg = Symbol_Pos.!!! ("Outer lexical error: " ^ msg);
+
+
+(* scan symbolic idents *)
+
+val is_sym_char = member (op =) (explode "!#$%&*+-/<=>?@^_|~");
+
+val scan_symid =
+  Scan.many1 (is_sym_char o symbol) ||
+  Scan.one (Symbol.is_symbolic o symbol) >> single;
+
+fun is_symid str =
+  (case try Symbol.explode str of
+    SOME [s] => Symbol.is_symbolic s orelse is_sym_char s
+  | SOME ss => forall is_sym_char ss
+  | _ => false);
+
+fun ident_or_symbolic "begin" = false
+  | ident_or_symbolic ":" = true
+  | ident_or_symbolic "::" = true
+  | ident_or_symbolic s = Syntax.is_identifier s orelse is_symid s;
+
+
+(* scan verbatim text *)
+
+val scan_verb =
+  $$$ "*" --| Scan.ahead (~$$$ "}") ||
+  Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s) >> single;
+
+val scan_verbatim =
+  (Symbol_Pos.scan_pos --| $$$ "{" --| $$$ "*") -- !!! "missing end of verbatim text"
+    (Symbol_Pos.change_prompt
+      ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- Symbol_Pos.scan_pos)));
+
+
+(* scan space *)
+
+fun is_space s = Symbol.is_blank s andalso s <> "\n";
+
+val scan_space =
+  Scan.many1 (is_space o symbol) @@@ Scan.optional ($$$ "\n") [] ||
+  Scan.many (is_space o symbol) @@@ $$$ "\n";
+
+
+(* scan comment *)
+
+val scan_comment =
+  Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body !!! -- Symbol_Pos.scan_pos);
+
+
+(* scan malformed symbols *)
+
+val scan_malformed =
+  $$$ Symbol.malformed |--
+    Symbol_Pos.change_prompt (Scan.many (Symbol.is_regular o symbol))
+  --| Scan.option ($$$ Symbol.end_malformed);
+
+
+
+(** token sources **)
+
+fun source_proper src = src |> Source.filter is_proper;
+
+local
+
+fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2;
+
+fun token k ss =
+  Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.untabify_content ss), Slot);
+
+fun token_range k (pos1, (ss, pos2)) =
+  Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.untabify_content ss), Slot);
+
+fun scan (lex1, lex2) = !!! "bad input"
+  (Symbol_Pos.scan_string >> token_range String ||
+    Symbol_Pos.scan_alt_string >> token_range AltString ||
+    scan_verbatim >> token_range Verbatim ||
+    scan_comment >> token_range Comment ||
+    scan_space >> token Space ||
+    scan_malformed >> token Malformed ||
+    Scan.one (Symbol.is_sync o symbol) >> (token Sync o single) ||
+    (Scan.max token_leq
+      (Scan.max token_leq
+        (Scan.literal lex2 >> pair Command)
+        (Scan.literal lex1 >> pair Keyword))
+      (Syntax.scan_longid >> pair LongIdent ||
+        Syntax.scan_id >> pair Ident ||
+        Syntax.scan_var >> pair Var ||
+        Syntax.scan_tid >> pair TypeIdent ||
+        Syntax.scan_tvar >> pair TypeVar ||
+        Syntax.scan_nat >> pair Nat ||
+        scan_symid >> pair SymIdent) >> uncurry token));
+
+fun recover msg =
+  Scan.many ((Symbol.is_regular andf (not o Symbol.is_blank)) o symbol)
+  >> (single o token (Error msg));
+
+in
+
+fun source' {do_recover} get_lex =
+  Source.source Symbol_Pos.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
+    (Option.map (rpair recover) do_recover);
+
+fun source do_recover get_lex pos src =
+  Symbol_Pos.source pos src
+  |> source' do_recover get_lex;
+
+end;
+
+
+(* read_antiq *)
+
+fun read_antiq lex scan (syms, pos) =
+  let
+    fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.str_of pos ^ ":\n" ^
+      "@{" ^ Symbol_Pos.content syms ^ "}");
+
+    val res =
+      Source.of_list syms
+      |> source' {do_recover = NONE} (K (lex, Scan.empty_lexicon))
+      |> source_proper
+      |> Source.source stopper (Scan.error (Scan.bulk scan)) NONE
+      |> Source.exhaust;
+  in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;
+
+end;
diff -r 71c8973a604b -r 4ec5131c6f46 src/Pure/Isar/token.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/token.scala	Tue May 18 06:28:42 2010 -0700
@@ -0,0 +1,95 @@
+/*  Title:      Pure/Isar/token.scala
+    Author:     Makarius
+
+Outer token syntax for Isabelle/Isar.
+*/
+
+package isabelle
+
+
+object Token
+{
+  /* tokens */
+
+  object Kind extends Enumeration
+  {
+    val COMMAND = Value("command")
+    val KEYWORD = Value("keyword")
+    val IDENT = Value("identifier")
+    val LONG_IDENT = Value("long identifier")
+    val SYM_IDENT = Value("symbolic identifier")
+    val VAR = Value("schematic variable")
+    val TYPE_IDENT = Value("type variable")
+    val TYPE_VAR = Value("schematic type variable")
+    val NAT = Value("number")
+    val STRING = Value("string")
+    val ALT_STRING = Value("back-quoted string")
+    val VERBATIM = Value("verbatim text")
+    val SPACE = Value("white space")
+    val COMMENT = Value("comment text")
+    val BAD_INPUT = Value("bad input")
+    val UNPARSED = Value("unparsed input")
+  }
+
+
+  /* token reader */
+
+  class Line_Position(val line: Int) extends scala.util.parsing.input.Position
+  {
+    def column = 0
+    def lineContents = ""
+    override def toString = line.toString
+
+    def advance(token: Token): Line_Position =
+    {
+      var n = 0
+      for (c <- token.content if c == '\n') n += 1
+      if (n == 0) this else new Line_Position(line + n)
+    }
+  }
+
+  abstract class Reader extends scala.util.parsing.input.Reader[Token]
+
+  private class Token_Reader(tokens: List[Token], val pos: Line_Position) extends Reader
+  {
+    def first = tokens.head
+    def rest = new Token_Reader(tokens.tail, pos.advance(first))
+    def atEnd = tokens.isEmpty
+  }
+
+  def reader(tokens: List[Token]): Reader = new Token_Reader(tokens, new Line_Position(1))
+}
+
+
+sealed case class Token(val kind: Token.Kind.Value, val source: String)
+{
+  def is_command: Boolean = kind == Token.Kind.COMMAND
+  def is_delimited: Boolean =
+    kind == Token.Kind.STRING ||
+    kind == Token.Kind.ALT_STRING ||
+    kind == Token.Kind.VERBATIM ||
+    kind == Token.Kind.COMMENT
+  def is_name: Boolean =
+    kind == Token.Kind.IDENT ||
+    kind == Token.Kind.SYM_IDENT ||
+    kind == Token.Kind.STRING ||
+    kind == Token.Kind.NAT
+  def is_xname: Boolean = is_name || kind == Token.Kind.LONG_IDENT
+  def is_text: Boolean = is_xname || kind == Token.Kind.VERBATIM
+  def is_space: Boolean = kind == Token.Kind.SPACE
+  def is_comment: Boolean = kind == Token.Kind.COMMENT
+  def is_ignored: Boolean = is_space || is_comment
+  def is_unparsed: Boolean = kind == Token.Kind.UNPARSED
+
+  def content: String =
+    if (kind == Token.Kind.STRING) Scan.Lexicon.empty.quoted_content("\"", source)
+    else if (kind == Token.Kind.ALT_STRING) Scan.Lexicon.empty.quoted_content("`", source)
+    else if (kind == Token.Kind.VERBATIM) Scan.Lexicon.empty.verbatim_content(source)
+    else if (kind == Token.Kind.COMMENT) Scan.Lexicon.empty.comment_content(source)
+    else source
+
+  def text: (String, String) =
+    if (kind == Token.Kind.COMMAND && source == ";") ("terminator", "")
+    else (kind.toString, source)
+}
+
diff -r 71c8973a604b -r 4ec5131c6f46 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/ML/ml_context.ML	Tue May 18 06:28:42 2010 -0700
@@ -112,8 +112,6 @@
 
 local
 
-structure T = OuterLex;
-
 val antiq =
   Parse.!!! (Parse.position Parse.xname -- Args.parse --| Scan.ahead Parse.eof)
   >> (fn ((x, pos), y) => Args.src ((x, y), pos));
@@ -144,7 +142,8 @@
             | expand (Antiquote.Antiq (ss, range)) (scope, background) =
                 let
                   val context = Stack.top scope;
-                  val (f, context') = antiquotation (T.read_antiq lex antiq (ss, #1 range)) context;
+                  val (f, context') =
+                    antiquotation (Token.read_antiq lex antiq (ss, #1 range)) context;
                   val (decl, background') = f background;
                   val decl' = decl #> pairself (ML_Lex.tokenize #> map (ML_Lex.set_range range));
                 in (decl', (Stack.map_top (K context') scope, background')) end
diff -r 71c8973a604b -r 4ec5131c6f46 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/PIDE/document.scala	Tue May 18 06:28:42 2010 -0700
@@ -46,7 +46,7 @@
     /* unparsed dummy commands */
 
     def unparsed(source: String) =
-      new Command(null, List(Outer_Lex.Token(Outer_Lex.Token_Kind.UNPARSED, source)))
+      new Command(null, List(Token(Token.Kind.UNPARSED, source)))
 
     def is_unparsed(command: Command) = command.id == null
 
diff -r 71c8973a604b -r 4ec5131c6f46 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/ROOT.ML	Tue May 18 06:28:42 2010 -0700
@@ -167,7 +167,7 @@
 use "Proof/proofchecker.ML";
 
 (*outer syntax*)
-use "Isar/outer_lex.ML";
+use "Isar/token.ML";
 use "Isar/keyword.ML";
 use "Isar/parse.ML";
 use "Isar/parse_value.ML";
@@ -292,3 +292,23 @@
 
 use "pure_setup.ML";
 
+
+(* legacy aliases *)
+
+structure Legacy =
+struct
+
+structure OuterKeyword = Keyword;
+
+structure OuterLex =
+struct
+  open Token;
+  type token = T;
+end;
+
+structure OuterParse = Parse;
+structure OuterSyntax = Outer_Syntax;
+structure SpecParse = Parse_Spec;
+
+end;
+
diff -r 71c8973a604b -r 4ec5131c6f46 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Thy/latex.ML	Tue May 18 06:28:42 2010 -0700
@@ -9,7 +9,7 @@
   val output_known_symbols: (string -> bool) * (string -> bool) ->
     Symbol.symbol list -> string
   val output_symbols: Symbol.symbol list -> string
-  val output_basic: OuterLex.token -> string
+  val output_basic: Token.T -> string
   val output_markup: string -> string -> string
   val output_markup_env: string -> string -> string
   val output_verbatim: string -> string
@@ -99,24 +99,22 @@
 
 (* token output *)
 
-structure T = OuterLex;
-
-val invisible_token = T.keyword_with (fn s => s = ";") orf T.is_kind T.Comment;
+val invisible_token = Token.keyword_with (fn s => s = ";") orf Token.is_kind Token.Comment;
 
 fun output_basic tok =
-  let val s = T.content_of tok in
+  let val s = Token.content_of tok in
     if invisible_token tok then ""
-    else if T.is_kind T.Command tok then
+    else if Token.is_kind Token.Command tok then
       "\\isacommand{" ^ output_syms s ^ "}"
-    else if T.is_kind T.Keyword tok andalso Syntax.is_ascii_identifier s then
+    else if Token.is_kind Token.Keyword tok andalso Syntax.is_ascii_identifier s then
       "\\isakeyword{" ^ output_syms s ^ "}"
-    else if T.is_kind T.String tok then
+    else if Token.is_kind Token.String tok then
       enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
-    else if T.is_kind T.AltString tok then
+    else if Token.is_kind Token.AltString tok then
       enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
-    else if T.is_kind T.Verbatim tok then
+    else if Token.is_kind Token.Verbatim tok then
       let
-        val (txt, pos) = T.source_position_of tok;
+        val (txt, pos) = Token.source_position_of tok;
         val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
         val out = implode (map output_syms_antiq ants);
       in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
diff -r 71c8973a604b -r 4ec5131c6f46 src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Thy/thy_header.ML	Tue May 18 06:28:42 2010 -0700
@@ -6,17 +6,13 @@
 
 signature THY_HEADER =
 sig
-  val args: OuterLex.token list ->
-    (string * string list * (string * bool) list) * OuterLex.token list
+  val args: Token.T list -> (string * string list * (string * bool) list) * Token.T list
   val read: Position.T -> (string, 'a) Source.source -> string * string list * (string * bool) list
 end;
 
 structure Thy_Header: THY_HEADER =
 struct
 
-structure T = OuterLex;
-
-
 (* keywords *)
 
 val headerN = "header";
@@ -58,9 +54,9 @@
   let val res =
     src
     |> Symbol.source {do_recover = false}
-    |> T.source {do_recover = NONE} (fn () => (header_lexicon, Scan.empty_lexicon)) pos
-    |> T.source_proper
-    |> Source.source T.stopper (Scan.single (Scan.error (Parse.!!! header))) NONE
+    |> Token.source {do_recover = NONE} (fn () => (header_lexicon, Scan.empty_lexicon)) pos
+    |> Token.source_proper
+    |> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header))) NONE
     |> Source.get_single;
   in
     (case res of SOME (x, _) => x
diff -r 71c8973a604b -r 4ec5131c6f46 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Thy/thy_header.scala	Tue May 18 06:28:42 2010 -0700
@@ -59,14 +59,14 @@
   def read(file: File): Header =
   {
     val token = lexicon.token(symbols, _ => false)
-    val toks = new mutable.ListBuffer[Outer_Lex.Token]
+    val toks = new mutable.ListBuffer[Token]
 
     def scan_to_begin(in: Reader[Char])
     {
       token(in) match {
         case lexicon.Success(tok, rest) =>
           toks += tok
-          if (!(tok.kind == Outer_Lex.Token_Kind.KEYWORD && tok.content == BEGIN))
+          if (!(tok.kind == Token.Kind.KEYWORD && tok.content == BEGIN))
             scan_to_begin(rest)
         case _ =>
       }
@@ -74,7 +74,7 @@
     val reader = Scan.byte_reader(file)
     try { scan_to_begin(reader) } finally { reader.close }
 
-    parse(commit(header), Outer_Lex.reader(toks.toList)) match {
+    parse(commit(header), Token.reader(toks.toList)) match {
       case Success(result, _) => result
       case bad => error(bad.toString)
     }
diff -r 71c8973a604b -r 4ec5131c6f46 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Thy/thy_output.ML	Tue May 18 06:28:42 2010 -0700
@@ -24,7 +24,7 @@
   val modes: string list Unsynchronized.ref
   val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
   val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
-    (Toplevel.transition * Toplevel.state) list -> (OuterLex.token, 'a) Source.source -> Buffer.T
+    (Toplevel.transition * Toplevel.state) list -> (Token.T, 'a) Source.source -> Buffer.T
   val pretty_text: string -> Pretty.T
   val pretty_term: Proof.context -> term -> Pretty.T
   val pretty_thm: Proof.context -> thm -> Pretty.T
@@ -36,9 +36,6 @@
 structure ThyOutput: THY_OUTPUT =
 struct
 
-structure T = OuterLex;
-
-
 (** global options **)
 
 val display = Unsynchronized.ref false;
@@ -154,7 +151,7 @@
   let
     fun expand (Antiquote.Text ss) = Symbol_Pos.content ss
       | expand (Antiquote.Antiq (ss, (pos, _))) =
-          let val (opts, src) = T.read_antiq lex antiq (ss, pos) in
+          let val (opts, src) = Token.read_antiq lex antiq (ss, pos) in
             options opts (fn () => command src state) ();  (*preview errors!*)
             PrintMode.with_modes (! modes @ Latex.modes)
               (Output.no_warnings_CRITICAL (options opts (fn () => command src state))) ()
@@ -178,7 +175,7 @@
 
 datatype token =
     NoToken
-  | BasicToken of T.token
+  | BasicToken of Token.T
   | MarkupToken of string * (string * Position.T)
   | MarkupEnvToken of string * (string * Position.T)
   | VerbatimToken of string * Position.T;
@@ -195,10 +192,10 @@
 fun basic_token pred (BasicToken tok) = pred tok
   | basic_token _ _ = false;
 
-val improper_token = basic_token (not o T.is_proper);
-val comment_token = basic_token T.is_comment;
-val blank_token = basic_token T.is_blank;
-val newline_token = basic_token T.is_newline;
+val improper_token = basic_token (not o Token.is_proper);
+val comment_token = basic_token Token.is_comment;
+val blank_token = basic_token Token.is_blank;
+val newline_token = basic_token Token.is_newline;
 
 
 (* command spans *)
@@ -303,19 +300,19 @@
 local
 
 val space_proper =
-  Scan.one T.is_blank -- Scan.many T.is_comment -- Scan.one T.is_proper;
+  Scan.one Token.is_blank -- Scan.many Token.is_comment -- Scan.one Token.is_proper;
 
-val is_improper = not o (T.is_proper orf T.is_begin_ignore orf T.is_end_ignore);
+val is_improper = not o (Token.is_proper orf Token.is_begin_ignore orf Token.is_end_ignore);
 val improper = Scan.many is_improper;
 val improper_end = Scan.repeat (Scan.unless space_proper (Scan.one is_improper));
-val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one T.is_blank));
+val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one Token.is_blank));
 
-val opt_newline = Scan.option (Scan.one T.is_newline);
+val opt_newline = Scan.option (Scan.one Token.is_newline);
 
 val ignore =
-  Scan.depend (fn d => opt_newline |-- Scan.one T.is_begin_ignore
+  Scan.depend (fn d => opt_newline |-- Scan.one Token.is_begin_ignore
     >> pair (d + 1)) ||
-  Scan.depend (fn d => Scan.one T.is_end_ignore --|
+  Scan.depend (fn d => Scan.one Token.is_end_ignore --|
     (if d = 0 then Scan.fail_with (K "Bad nesting of meta-comments") else opt_newline)
     >> pair (d - 1));
 
@@ -336,18 +333,19 @@
 
     fun markup mark mk flag = Scan.peek (fn d =>
       improper |--
-        Parse.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.content_of)) --
+        Parse.position
+          (Scan.one (Token.is_kind Token.Command andf is_markup mark o Token.content_of)) --
       Scan.repeat tag --
       Parse.!!!! ((improper -- locale -- improper) |-- Parse.doc_source --| improper_end)
       >> (fn (((tok, pos), tags), txt) =>
-        let val name = T.content_of tok
+        let val name = Token.content_of tok
         in (SOME (name, pos, tags), (mk (name, txt), (flag, d))) end));
 
     val command = Scan.peek (fn d =>
-      Parse.position (Scan.one (T.is_kind T.Command)) --
+      Parse.position (Scan.one (Token.is_kind Token.Command)) --
       Scan.repeat tag
       >> (fn ((tok, pos), tags) =>
-        let val name = T.content_of tok
+        let val name = Token.content_of tok
         in (SOME (name, pos, tags), (BasicToken tok, (Latex.markup_false, d))) end));
 
     val cmt = Scan.peek (fn d =>
@@ -367,8 +365,8 @@
 
     (* spans *)
 
-    val is_eof = fn (_, (BasicToken x, _)) => T.is_eof x | _ => false;
-    val stopper = Scan.stopper (K (NONE, (BasicToken T.eof, ("", 0)))) is_eof;
+    val is_eof = fn (_, (BasicToken x, _)) => Token.is_eof x | _ => false;
+    val stopper = Scan.stopper (K (NONE, (BasicToken Token.eof, ("", 0)))) is_eof;
 
     val cmd = Scan.one (is_some o fst);
     val non_cmd = Scan.one (is_none o fst andf not o is_eof) >> #2;
@@ -390,8 +388,8 @@
 
     val spans =
       src
-      |> Source.filter (not o T.is_semicolon)
-      |> Source.source' 0 T.stopper (Scan.error (Scan.bulk token)) NONE
+      |> Source.filter (not o Token.is_semicolon)
+      |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk token)) NONE
       |> Source.source stopper (Scan.error (Scan.bulk span)) NONE
       |> Source.exhaust;
 
@@ -490,7 +488,7 @@
 
 (* default output *)
 
-val str_of_source = space_implode " " o map T.unparse o #2 o #1 o Args.dest_src;
+val str_of_source = space_implode " " o map Token.unparse o #2 o #1 o Args.dest_src;
 
 fun maybe_pretty_source pretty src xs =
   map pretty xs  (*always pretty in order to exhibit errors!*)
diff -r 71c8973a604b -r 4ec5131c6f46 src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Thy/thy_syntax.ML	Tue May 18 06:28:42 2010 -0700
@@ -7,18 +7,17 @@
 signature THY_SYNTAX =
 sig
   val token_source: Scan.lexicon * Scan.lexicon -> Position.T -> (string, 'a) Source.source ->
-    (OuterLex.token, (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, 'a)
+    (Token.T, (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, 'a)
       Source.source) Source.source) Source.source) Source.source
-  val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> OuterLex.token list
-  val present_token: OuterLex.token -> output
-  val report_token: OuterLex.token -> unit
+  val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
+  val present_token: Token.T -> output
+  val report_token: Token.T -> unit
   datatype span_kind = Command of string | Ignored | Malformed
   type span
   val span_kind: span -> span_kind
-  val span_content: span -> OuterLex.token list
+  val span_content: span -> Token.T list
   val span_range: span -> Position.range
-  val span_source: (OuterLex.token, 'a) Source.source ->
-    (span, (OuterLex.token, 'a) Source.source) Source.source
+  val span_source: (Token.T, 'a) Source.source -> (span, (Token.T, 'a) Source.source) Source.source
   val parse_spans: Scan.lexicon * Scan.lexicon -> Position.T -> string -> span list
   val present_span: span -> output
   val report_span: span -> unit
@@ -29,16 +28,13 @@
 structure ThySyntax: THY_SYNTAX =
 struct
 
-structure T = OuterLex;
-
-
 (** tokens **)
 
 (* parse *)
 
 fun token_source lexs pos src =
   Symbol.source {do_recover = true} src
-  |> T.source {do_recover = SOME false} (K lexs) pos;
+  |> Token.source {do_recover = SOME false} (K lexs) pos;
 
 fun parse_tokens lexs pos str =
   Source.of_string str
@@ -51,33 +47,33 @@
 local
 
 val token_kind_markup =
- fn T.Command       => (Markup.commandN, [])
-  | T.Keyword       => (Markup.keywordN, [])
-  | T.Ident         => Markup.ident
-  | T.LongIdent     => Markup.ident
-  | T.SymIdent      => Markup.ident
-  | T.Var           => Markup.var
-  | T.TypeIdent     => Markup.tfree
-  | T.TypeVar       => Markup.tvar
-  | T.Nat           => Markup.ident
-  | T.String        => Markup.string
-  | T.AltString     => Markup.altstring
-  | T.Verbatim      => Markup.verbatim
-  | T.Space         => Markup.none
-  | T.Comment       => Markup.comment
-  | T.InternalValue => Markup.none
-  | T.Malformed     => Markup.malformed
-  | T.Error _       => Markup.malformed
-  | T.Sync          => Markup.control
-  | T.EOF           => Markup.control;
+ fn Token.Command       => (Markup.commandN, [])
+  | Token.Keyword       => (Markup.keywordN, [])
+  | Token.Ident         => Markup.ident
+  | Token.LongIdent     => Markup.ident
+  | Token.SymIdent      => Markup.ident
+  | Token.Var           => Markup.var
+  | Token.TypeIdent     => Markup.tfree
+  | Token.TypeVar       => Markup.tvar
+  | Token.Nat           => Markup.ident
+  | Token.String        => Markup.string
+  | Token.AltString     => Markup.altstring
+  | Token.Verbatim      => Markup.verbatim
+  | Token.Space         => Markup.none
+  | Token.Comment       => Markup.comment
+  | Token.InternalValue => Markup.none
+  | Token.Malformed     => Markup.malformed
+  | Token.Error _       => Markup.malformed
+  | Token.Sync          => Markup.control
+  | Token.EOF           => Markup.control;
 
 in
 
 fun present_token tok =
-  Markup.enclose (token_kind_markup (T.kind_of tok)) (Output.output (T.unparse tok));
+  Markup.enclose (token_kind_markup (Token.kind_of tok)) (Output.output (Token.unparse tok));
 
 fun report_token tok =
-  Position.report (token_kind_markup (T.kind_of tok)) (T.position_of tok);
+  Position.report (token_kind_markup (Token.kind_of tok)) (Token.position_of tok);
 
 end;
 
@@ -88,7 +84,7 @@
 (* type span *)
 
 datatype span_kind = Command of string | Ignored | Malformed;
-datatype span = Span of span_kind * OuterLex.token list;
+datatype span = Span of span_kind * Token.T list;
 
 fun span_kind (Span (k, _)) = k;
 fun span_content (Span (_, toks)) = toks;
@@ -98,8 +94,8 @@
     [] => (Position.none, Position.none)
   | toks =>
       let
-        val start_pos = T.position_of (hd toks);
-        val end_pos = T.end_position_of (List.last toks);
+        val start_pos = Token.position_of (hd toks);
+        val end_pos = Token.end_position_of (List.last toks);
       in (start_pos, end_pos) end);
 
 
@@ -107,7 +103,7 @@
 
 local
 
-val is_whitespace = T.is_kind T.Space orf T.is_kind T.Comment;
+val is_whitespace = Token.is_kind Token.Space orf Token.is_kind Token.Comment;
 
 val body =
   Scan.unless (Scan.many is_whitespace -- Scan.ahead (Parse.command || Parse.eof)) Parse.not_eof;
@@ -120,7 +116,7 @@
 
 in
 
-fun span_source src = Source.source T.stopper (Scan.bulk span) NONE src;
+fun span_source src = Source.source Token.stopper (Scan.bulk span) NONE src;
 
 end;
 
diff -r 71c8973a604b -r 4ec5131c6f46 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Thy/thy_syntax.scala	Tue May 18 06:28:42 2010 -0700
@@ -22,13 +22,13 @@
     }
   }
 
-  type Span = List[Outer_Lex.Token]
+  type Span = List[Token]
 
-  def parse_spans(toks: List[Outer_Lex.Token]): List[Span] =
+  def parse_spans(toks: List[Token]): List[Span] =
   {
     import parser._
 
-    parse(rep(command_span), Outer_Lex.reader(toks)) match {
+    parse(rep(command_span), Token.reader(toks)) match {
       case Success(spans, rest) if rest.atEnd => spans
       case bad => error(bad.toString)
     }
diff -r 71c8973a604b -r 4ec5131c6f46 src/Pure/build-jars
--- a/src/Pure/build-jars	Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/build-jars	Tue May 18 06:28:42 2010 -0700
@@ -34,9 +34,9 @@
   General/yxml.scala
   Isar/isar_document.scala
   Isar/keyword.scala
-  Isar/outer_lex.scala
   Isar/outer_syntax.scala
   Isar/parse.scala
+  Isar/token.scala
   PIDE/change.scala
   PIDE/command.scala
   PIDE/document.scala
diff -r 71c8973a604b -r 4ec5131c6f46 src/Tools/Code/code_eval.ML
--- a/src/Tools/Code/code_eval.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Tools/Code/code_eval.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Tools/Code/code_haskell.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Tools/Code/code_preproc.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Tools/Code/code_printer.ML	Tue May 18 06:28:42 2010 -0700
@@ -72,9 +72,9 @@
   val parse_infix: ('a -> 'b) -> lrx * int -> string
     -> int * ((fixity -> 'b -> Pretty.T)
     -> fixity -> 'a list -> Pretty.T)
-  val parse_syntax: ('a -> 'b) -> OuterParse.token list
+  val parse_syntax: ('a -> 'b) -> Token.T list
     -> (int * ((fixity -> 'b -> Pretty.T)
-    -> fixity -> 'a list -> Pretty.T)) option * OuterParse.token list
+    -> fixity -> 'a list -> Pretty.T)) option * Token.T list
   val simple_const_syntax: simple_const_syntax -> proto_const_syntax
   val activate_const_syntax: theory -> literals
     -> proto_const_syntax -> Code_Thingol.naming -> const_syntax * Code_Thingol.naming
@@ -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 71c8973a604b -r 4ec5131c6f46 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Tools/Code/code_target.ML	Tue May 18 06:28:42 2010 -0700
@@ -19,14 +19,13 @@
 
   type destination
   type serialization
-  val parse_args: (OuterLex.token list -> 'a * OuterLex.token list)
-    -> OuterLex.token list -> 'a
+  val parse_args: 'a parser -> Token.T list -> 'a
   val stmt_names_of_destination: destination -> string list
   val mk_serialization: string -> ('a -> unit) option
     -> (Path.T option -> 'a -> unit)
     -> ('a -> string * string option list)
     -> 'a -> serialization
-  val serialize: theory -> string -> int option -> string option -> OuterLex.token list
+  val serialize: theory -> string -> int option -> string option -> Token.T list
     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
   val serialize_custom: theory -> string * (serializer * literals)
     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
@@ -105,7 +104,7 @@
 
 type serializer =
   string option                         (*module name*)
-  -> OuterLex.token list                (*arguments*)
+  -> Token.T list                       (*arguments*)
   -> (string -> string)                 (*labelled_name*)
   -> string list                        (*reserved symbols*)
   -> (string * Pretty.T) list           (*includes*)
@@ -464,9 +463,6 @@
 
 local
 
-structure P = OuterParse
-and K = OuterKeyword
-
 fun zip_list (x::xs) f g =
   f
   #-> (fn y =>
@@ -474,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
 
@@ -498,7 +494,7 @@
 val allow_abort_cmd = gen_allow_abort Code.read_const;
 
 fun parse_args f args =
-  case Scan.read OuterLex.stopper f args
+  case Scan.read Token.stopper f args
    of SOME x => x
     | NONE => error "Bad serializer arguments";
 
@@ -508,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 OuterLex.stopper (P.!!! code_exprP)
-    ((filter OuterLex.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 71c8973a604b -r 4ec5131c6f46 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Tools/Code/code_thingol.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/Tools/WWW_Find/find_theorems.ML
--- a/src/Tools/WWW_Find/find_theorems.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Tools/WWW_Find/find_theorems.ML	Tue May 18 06:28:42 2010 -0700
@@ -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,8 +190,8 @@
     fun get_query () =
       query
       |> (fn s => s ^ ";")
-      |> OuterSyntax.scan Position.start
-      |> filter OuterLex.is_proper
+      |> Outer_Syntax.scan Position.start
+      |> filter Token.is_proper
       |> Scan.error parse_query
       |> fst;
 
diff -r 71c8973a604b -r 4ec5131c6f46 src/Tools/WWW_Find/unicode_symbols.ML
--- a/src/Tools/WWW_Find/unicode_symbols.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Tools/WWW_Find/unicode_symbols.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/Tools/eqsubst.ML
--- a/src/Tools/eqsubst.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Tools/eqsubst.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Tools/induct.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/Tools/induct_tacs.ML
--- a/src/Tools/induct_tacs.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Tools/induct_tacs.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/Tools/intuitionistic.ML
--- a/src/Tools/intuitionistic.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Tools/intuitionistic.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Tools/nbe.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Tools/quickcheck.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/Tools/value.ML
--- a/src/Tools/value.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/Tools/value.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/ZF/Tools/datatype_package.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/ZF/Tools/ind_cases.ML
--- a/src/ZF/Tools/ind_cases.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/ZF/Tools/ind_cases.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/ZF/Tools/induct_tacs.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/ZF/Tools/inductive_package.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/ZF/Tools/primrec_package.ML	Tue May 18 06:28:42 2010 -0700
@@ -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 71c8973a604b -r 4ec5131c6f46 src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Mon May 17 18:59:59 2010 -0700
+++ b/src/ZF/Tools/typechk.ML	Tue May 18 06:28:42 2010 -0700
@@ -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)));