prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
authorwenzelm
Mon May 17 23:54:15 2010 +0200 (2010-05-17)
changeset 3696001594f816e3a
parent 36959 f5417836dbea
child 36961 7b14afc02fc4
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
eliminated old-style structure aliases K = Keyword, P = Parse;
src/FOL/ex/Iff_Oracle.thy
src/HOL/Boogie/Tools/boogie_commands.ML
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Import/import_syntax.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_induct.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Orderings.thy
src/HOL/Statespace/state_space.ML
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/datatype_data.ML
src/HOL/Tools/Function/fun.ML
src/HOL/Tools/Function/function.ML
src/HOL/Tools/Function/function_common.ML
src/HOL/Tools/Nitpick/nitpick_isar.ML
src/HOL/Tools/Predicate_Compile/predicate_compile.ML
src/HOL/Tools/Quotient/quotient_def.ML
src/HOL/Tools/Quotient/quotient_info.ML
src/HOL/Tools/Quotient/quotient_typ.ML
src/HOL/Tools/SMT/smt_solver.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
src/HOL/Tools/choice_specification.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/primrec.ML
src/HOL/Tools/recdef.ML
src/HOL/Tools/record.ML
src/HOL/Tools/refute_isar.ML
src/HOL/Tools/split_rule.ML
src/HOL/Tools/typedef.ML
src/HOLCF/IOA/meta_theory/automaton.ML
src/HOLCF/Tools/Domain/domain_extender.ML
src/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOLCF/Tools/cont_consts.ML
src/HOLCF/Tools/fixrec.ML
src/HOLCF/Tools/pcpodef.ML
src/HOLCF/Tools/repdef.ML
src/Provers/blast.ML
src/Provers/clasimp.ML
src/Provers/classical.ML
src/Tools/Code/code_eval.ML
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_printer.ML
src/Tools/Code/code_target.ML
src/Tools/Code/code_thingol.ML
src/Tools/WWW_Find/find_theorems.ML
src/Tools/WWW_Find/unicode_symbols.ML
src/Tools/eqsubst.ML
src/Tools/induct.ML
src/Tools/induct_tacs.ML
src/Tools/intuitionistic.ML
src/Tools/nbe.ML
src/Tools/quickcheck.ML
src/Tools/value.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/ind_cases.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/primrec_package.ML
src/ZF/Tools/typechk.ML
     1.1 --- a/src/FOL/ex/Iff_Oracle.thy	Mon May 17 15:11:25 2010 +0200
     1.2 +++ b/src/FOL/ex/Iff_Oracle.thy	Mon May 17 23:54:15 2010 +0200
     1.3 @@ -52,7 +52,7 @@
     1.4  subsection {* Oracle as proof method *}
     1.5  
     1.6  method_setup iff = {*
     1.7 -  Scan.lift OuterParse.nat >> (fn n => fn ctxt =>
     1.8 +  Scan.lift Parse.nat >> (fn n => fn ctxt =>
     1.9      SIMPLE_METHOD
    1.10        (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt, n)))
    1.11          handle Fail _ => no_tac))
     2.1 --- a/src/HOL/Boogie/Tools/boogie_commands.ML	Mon May 17 15:11:25 2010 +0200
     2.2 +++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Mon May 17 23:54:15 2010 +0200
     2.3 @@ -263,31 +263,31 @@
     2.4  fun scan_arg f = Args.parens f
     2.5  fun scan_opt n = Scan.optional (scan_arg (Args.$$$ n >> K true)) false
     2.6  
     2.7 -val vc_offsets = Scan.optional (Args.bracks (OuterParse.list1
     2.8 -  (OuterParse.string --| Args.colon -- OuterParse.nat))) []
     2.9 +val vc_offsets = Scan.optional (Args.bracks (Parse.list1
    2.10 +  (Parse.string --| Args.colon -- Parse.nat))) []
    2.11  
    2.12  val _ =
    2.13 -  OuterSyntax.command "boogie_open"
    2.14 +  Outer_Syntax.command "boogie_open"
    2.15      "Open a new Boogie environment and load a Boogie-generated .b2i file."
    2.16 -    OuterKeyword.thy_decl
    2.17 -    (scan_opt "quiet" -- OuterParse.name -- vc_offsets >> 
    2.18 +    Keyword.thy_decl
    2.19 +    (scan_opt "quiet" -- Parse.name -- vc_offsets >> 
    2.20        (Toplevel.theory o boogie_open))
    2.21  
    2.22  
    2.23 -val vc_name = OuterParse.name
    2.24 +val vc_name = Parse.name
    2.25  
    2.26 -val vc_label = OuterParse.name
    2.27 +val vc_label = Parse.name
    2.28  val vc_labels = Scan.repeat1 vc_label
    2.29  
    2.30  val vc_paths =
    2.31 -  OuterParse.nat -- (Args.$$$ "-" |-- OuterParse.nat) >> (op upto) ||
    2.32 -  OuterParse.nat >> single
    2.33 +  Parse.nat -- (Args.$$$ "-" |-- Parse.nat) >> (op upto) ||
    2.34 +  Parse.nat >> single
    2.35  
    2.36  val vc_opts =
    2.37    scan_arg
    2.38     (scan_val "assertion" vc_label >> VC_Single ||
    2.39      scan_val "examine" vc_labels >> VC_Examine ||
    2.40 -    scan_val "take" ((OuterParse.list vc_paths >> flat) -- Scan.option (
    2.41 +    scan_val "take" ((Parse.list vc_paths >> flat) -- Scan.option (
    2.42        scan_val "without" vc_labels >> pair false ||
    2.43        scan_val "and_also" vc_labels >> pair true) >> VC_Take) ||
    2.44      scan_val "only" vc_labels >> VC_Only ||
    2.45 @@ -295,9 +295,9 @@
    2.46    Scan.succeed VC_Complete
    2.47  
    2.48  val _ =
    2.49 -  OuterSyntax.command "boogie_vc"
    2.50 +  Outer_Syntax.command "boogie_vc"
    2.51      "Enter into proof mode for a specific verification condition."
    2.52 -    OuterKeyword.thy_goal
    2.53 +    Keyword.thy_goal
    2.54      (vc_name -- vc_opts >> (fn args =>
    2.55        (Toplevel.print o Toplevel.theory_to_proof (boogie_vc args))))
    2.56  
    2.57 @@ -305,7 +305,7 @@
    2.58  val quick_timeout = 5
    2.59  val default_timeout = 20
    2.60  
    2.61 -fun timeout name = Scan.optional (scan_val name OuterParse.nat)
    2.62 +fun timeout name = Scan.optional (scan_val name Parse.nat)
    2.63  
    2.64  val status_test =
    2.65    scan_arg (
    2.66 @@ -328,18 +328,18 @@
    2.67    f (Toplevel.theory_of state))
    2.68  
    2.69  val _ =
    2.70 -  OuterSyntax.improper_command "boogie_status"
    2.71 +  Outer_Syntax.improper_command "boogie_status"
    2.72      "Show the name and state of all loaded verification conditions."
    2.73 -    OuterKeyword.diag
    2.74 +    Keyword.diag
    2.75      (status_test >> status_cmd ||
    2.76       status_vc >> status_cmd ||
    2.77       Scan.succeed (status_cmd boogie_status))
    2.78  
    2.79  
    2.80  val _ =
    2.81 -  OuterSyntax.command "boogie_end"
    2.82 +  Outer_Syntax.command "boogie_end"
    2.83      "Close the current Boogie environment."
    2.84 -    OuterKeyword.thy_decl
    2.85 +    Keyword.thy_decl
    2.86      (Scan.succeed (Toplevel.theory boogie_end))
    2.87  
    2.88  
     3.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Mon May 17 15:11:25 2010 +0200
     3.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Mon May 17 23:54:15 2010 +0200
     3.3 @@ -3310,13 +3310,13 @@
     3.4    by auto
     3.5  
     3.6  method_setup approximation = {*
     3.7 -  Scan.lift (OuterParse.nat)
     3.8 +  Scan.lift Parse.nat
     3.9    --
    3.10    Scan.optional (Scan.lift (Args.$$$ "splitting" |-- Args.colon)
    3.11 -    |-- OuterParse.and_list' (free --| Scan.lift (Args.$$$ "=") -- Scan.lift OuterParse.nat)) []
    3.12 +    |-- Parse.and_list' (free --| Scan.lift (Args.$$$ "=") -- Scan.lift Parse.nat)) []
    3.13    --
    3.14    Scan.option (Scan.lift (Args.$$$ "taylor" |-- Args.colon)
    3.15 -    |-- (free |-- Scan.lift (Args.$$$ "=") |-- Scan.lift OuterParse.nat))
    3.16 +    |-- (free |-- Scan.lift (Args.$$$ "=") |-- Scan.lift Parse.nat))
    3.17    >>
    3.18    (fn ((prec, splitting), taylor) => fn ctxt =>
    3.19      SIMPLE_METHOD' (fn i =>
     4.1 --- a/src/HOL/Import/import_syntax.ML	Mon May 17 15:11:25 2010 +0200
     4.2 +++ b/src/HOL/Import/import_syntax.ML	Mon May 17 23:54:15 2010 +0200
     4.3 @@ -28,25 +28,23 @@
     4.4  structure HOL4ImportSyntax :> HOL4_IMPORT_SYNTAX =
     4.5  struct
     4.6  
     4.7 -local structure P = OuterParse and K = OuterKeyword in
     4.8 -
     4.9  (* Parsers *)
    4.10  
    4.11 -val import_segment = P.name >> set_import_segment
    4.12 +val import_segment = Parse.name >> set_import_segment
    4.13  
    4.14  
    4.15 -val import_theory = P.name >> (fn thyname =>
    4.16 +val import_theory = Parse.name >> (fn thyname =>
    4.17                                 fn thy =>
    4.18                                    thy |> set_generating_thy thyname
    4.19                                        |> Sign.add_path thyname
    4.20                                        |> add_dump (";setup_theory " ^ thyname))
    4.21  
    4.22  fun do_skip_import_dir s = (ImportRecorder.set_skip_import_dir (SOME s); I)
    4.23 -val skip_import_dir = P.string >> do_skip_import_dir
    4.24 +val skip_import_dir = Parse.string >> do_skip_import_dir
    4.25  
    4.26  val lower = String.map Char.toLower
    4.27  fun do_skip_import s = (ImportRecorder.set_skip_import (case lower s of "on" => true | "off" => false | _ => Scan.fail ()); I)
    4.28 -val skip_import = P.short_ident >> do_skip_import
    4.29 +val skip_import = Parse.short_ident >> do_skip_import
    4.30  
    4.31  fun end_import toks =
    4.32      Scan.succeed
    4.33 @@ -78,7 +76,7 @@
    4.34                      |> add_dump ";end_setup"
    4.35              end) toks
    4.36  
    4.37 -val ignore_thms = Scan.repeat1 P.name
    4.38 +val ignore_thms = Scan.repeat1 Parse.name
    4.39                                 >> (fn ignored =>
    4.40                                     fn thy =>
    4.41                                        let
    4.42 @@ -87,7 +85,7 @@
    4.43                                            Library.foldl (fn (thy,thmname) => ignore_hol4 thyname thmname thy) (thy,ignored)
    4.44                                        end)
    4.45  
    4.46 -val thm_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname)
    4.47 +val thm_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)
    4.48                              >> (fn thmmaps =>
    4.49                                  fn thy =>
    4.50                                     let
    4.51 @@ -96,7 +94,7 @@
    4.52                                         Library.foldl (fn (thy,(hol,isa)) => add_hol4_mapping thyname hol isa thy) (thy,thmmaps)
    4.53                                     end)
    4.54  
    4.55 -val type_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname)
    4.56 +val type_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)
    4.57                               >> (fn typmaps =>
    4.58                                   fn thy =>
    4.59                                      let
    4.60 @@ -105,7 +103,7 @@
    4.61                                          Library.foldl (fn (thy,(hol,isa)) => add_hol4_type_mapping thyname hol false isa thy) (thy,typmaps)
    4.62                                      end)
    4.63  
    4.64 -val def_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname)
    4.65 +val def_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)
    4.66                              >> (fn defmaps =>
    4.67                                  fn thy =>
    4.68                                     let
    4.69 @@ -114,7 +112,7 @@
    4.70                                         Library.foldl (fn (thy,(hol,isa)) => add_defmap thyname hol isa thy) (thy,defmaps)
    4.71                                     end)
    4.72  
    4.73 -val const_renames = Scan.repeat1 (P.name --| P.$$$ ">" -- P.name)
    4.74 +val const_renames = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.name)
    4.75                                   >> (fn renames =>
    4.76                                       fn thy =>
    4.77                                          let
    4.78 @@ -123,7 +121,7 @@
    4.79                                              Library.foldl (fn (thy,(hol,isa)) => add_hol4_const_renaming thyname hol isa thy) (thy,renames)
    4.80                                          end)
    4.81                                                                                                                                        
    4.82 -val const_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
    4.83 +val const_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname -- Scan.option (Parse.$$$ "::" |-- Parse.typ))
    4.84                                >> (fn constmaps =>
    4.85                                    fn thy =>
    4.86                                       let
    4.87 @@ -133,7 +131,7 @@
    4.88                                                   | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol false isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps)
    4.89                                       end)
    4.90  
    4.91 -val const_moves = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
    4.92 +val const_moves = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname -- Scan.option (Parse.$$$ "::" |-- Parse.typ))
    4.93                                 >> (fn constmaps =>
    4.94                                     fn thy =>
    4.95                                        let
    4.96 @@ -156,16 +154,16 @@
    4.97          val get_lexes = fn () => !lexes
    4.98          val token_source = Token.source {do_recover = NONE} get_lexes Position.start symb_source
    4.99          val token_list = filter_out (Token.is_kind Token.Space) (Source.exhaust token_source)
   4.100 -        val import_segmentP = OuterParse.$$$ "import_segment" |-- import_segment
   4.101 -        val type_mapsP = OuterParse.$$$ "type_maps" |-- type_maps
   4.102 -        val def_mapsP = OuterParse.$$$ "def_maps" |-- def_maps
   4.103 -        val const_mapsP = OuterParse.$$$ "const_maps" |-- const_maps
   4.104 -        val const_movesP = OuterParse.$$$ "const_moves" |-- const_moves
   4.105 -        val const_renamesP = OuterParse.$$$ "const_renames" |-- const_renames
   4.106 -        val ignore_thmsP = OuterParse.$$$ "ignore_thms" |-- ignore_thms
   4.107 -        val thm_mapsP = OuterParse.$$$ "thm_maps" |-- thm_maps
   4.108 +        val import_segmentP = Parse.$$$ "import_segment" |-- import_segment
   4.109 +        val type_mapsP = Parse.$$$ "type_maps" |-- type_maps
   4.110 +        val def_mapsP = Parse.$$$ "def_maps" |-- def_maps
   4.111 +        val const_mapsP = Parse.$$$ "const_maps" |-- const_maps
   4.112 +        val const_movesP = Parse.$$$ "const_moves" |-- const_moves
   4.113 +        val const_renamesP = Parse.$$$ "const_renames" |-- const_renames
   4.114 +        val ignore_thmsP = Parse.$$$ "ignore_thms" |-- ignore_thms
   4.115 +        val thm_mapsP = Parse.$$$ "thm_maps" |-- thm_maps
   4.116          val parser = type_mapsP || def_mapsP || const_mapsP || const_movesP || const_renamesP || thm_mapsP || ignore_thmsP || import_segmentP
   4.117 -        val importP = OuterParse.$$$ "import" |-- Scan.repeat parser --| OuterParse.$$$ "end"
   4.118 +        val importP = Parse.$$$ "import" |-- Scan.repeat parser --| Parse.$$$ "end"
   4.119          fun apply [] thy = thy
   4.120            | apply (f::fs) thy = apply fs (f thy)
   4.121      in
   4.122 @@ -188,7 +186,7 @@
   4.123              NONE => error "Import data already cleared - forgotten a setup_theory?"
   4.124            | SOME _ => ImportData.put NONE thy
   4.125  
   4.126 -val setup_theory = P.name
   4.127 +val setup_theory = Parse.name
   4.128                         >>
   4.129                         (fn thyname =>
   4.130                          fn thy =>
   4.131 @@ -212,64 +210,62 @@
   4.132                      |> Sign.parent_path
   4.133              end) toks
   4.134  
   4.135 -val set_dump  = P.string -- P.string   >> setup_dump
   4.136 +val set_dump  = Parse.string -- Parse.string   >> setup_dump
   4.137  fun fl_dump toks  = Scan.succeed flush_dump toks
   4.138 -val append_dump = (P.verbatim || P.string) >> add_dump
   4.139 +val append_dump = (Parse.verbatim || Parse.string) >> add_dump
   4.140  
   4.141  fun setup () =
   4.142 -  (OuterKeyword.keyword ">";
   4.143 -   OuterSyntax.command "import_segment"
   4.144 +  (Keyword.keyword ">";
   4.145 +   Outer_Syntax.command "import_segment"
   4.146                         "Set import segment name"
   4.147 -                       K.thy_decl (import_segment >> Toplevel.theory);
   4.148 -   OuterSyntax.command "import_theory"
   4.149 +                       Keyword.thy_decl (import_segment >> Toplevel.theory);
   4.150 +   Outer_Syntax.command "import_theory"
   4.151                         "Set default HOL4 theory name"
   4.152 -                       K.thy_decl (import_theory >> Toplevel.theory);
   4.153 -   OuterSyntax.command "end_import"
   4.154 +                       Keyword.thy_decl (import_theory >> Toplevel.theory);
   4.155 +   Outer_Syntax.command "end_import"
   4.156                         "End HOL4 import"
   4.157 -                       K.thy_decl (end_import >> Toplevel.theory);
   4.158 -   OuterSyntax.command "skip_import_dir" 
   4.159 +                       Keyword.thy_decl (end_import >> Toplevel.theory);
   4.160 +   Outer_Syntax.command "skip_import_dir" 
   4.161                         "Sets caching directory for skipping importing"
   4.162 -                       K.thy_decl (skip_import_dir >> Toplevel.theory);
   4.163 -   OuterSyntax.command "skip_import" 
   4.164 +                       Keyword.thy_decl (skip_import_dir >> Toplevel.theory);
   4.165 +   Outer_Syntax.command "skip_import" 
   4.166                         "Switches skipping importing on or off"
   4.167 -                       K.thy_decl (skip_import >> Toplevel.theory);                   
   4.168 -   OuterSyntax.command "setup_theory"
   4.169 +                       Keyword.thy_decl (skip_import >> Toplevel.theory);                   
   4.170 +   Outer_Syntax.command "setup_theory"
   4.171                         "Setup HOL4 theory replaying"
   4.172 -                       K.thy_decl (setup_theory >> Toplevel.theory);
   4.173 -   OuterSyntax.command "end_setup"
   4.174 +                       Keyword.thy_decl (setup_theory >> Toplevel.theory);
   4.175 +   Outer_Syntax.command "end_setup"
   4.176                         "End HOL4 setup"
   4.177 -                       K.thy_decl (end_setup >> Toplevel.theory);
   4.178 -   OuterSyntax.command "setup_dump"
   4.179 +                       Keyword.thy_decl (end_setup >> Toplevel.theory);
   4.180 +   Outer_Syntax.command "setup_dump"
   4.181                         "Setup the dump file name"
   4.182 -                       K.thy_decl (set_dump >> Toplevel.theory);
   4.183 -   OuterSyntax.command "append_dump"
   4.184 +                       Keyword.thy_decl (set_dump >> Toplevel.theory);
   4.185 +   Outer_Syntax.command "append_dump"
   4.186                         "Add text to dump file"
   4.187 -                       K.thy_decl (append_dump >> Toplevel.theory);
   4.188 -   OuterSyntax.command "flush_dump"
   4.189 +                       Keyword.thy_decl (append_dump >> Toplevel.theory);
   4.190 +   Outer_Syntax.command "flush_dump"
   4.191                         "Write the dump to file"
   4.192 -                       K.thy_decl (fl_dump >> Toplevel.theory);
   4.193 -   OuterSyntax.command "ignore_thms"
   4.194 +                       Keyword.thy_decl (fl_dump >> Toplevel.theory);
   4.195 +   Outer_Syntax.command "ignore_thms"
   4.196                         "Theorems to ignore in next HOL4 theory import"
   4.197 -                       K.thy_decl (ignore_thms >> Toplevel.theory);
   4.198 -   OuterSyntax.command "type_maps"
   4.199 +                       Keyword.thy_decl (ignore_thms >> Toplevel.theory);
   4.200 +   Outer_Syntax.command "type_maps"
   4.201                         "Map HOL4 type names to existing Isabelle/HOL type names"
   4.202 -                       K.thy_decl (type_maps >> Toplevel.theory);
   4.203 -   OuterSyntax.command "def_maps"
   4.204 +                       Keyword.thy_decl (type_maps >> Toplevel.theory);
   4.205 +   Outer_Syntax.command "def_maps"
   4.206                         "Map HOL4 constant names to their primitive definitions"
   4.207 -                       K.thy_decl (def_maps >> Toplevel.theory);
   4.208 -   OuterSyntax.command "thm_maps"
   4.209 +                       Keyword.thy_decl (def_maps >> Toplevel.theory);
   4.210 +   Outer_Syntax.command "thm_maps"
   4.211                         "Map HOL4 theorem names to existing Isabelle/HOL theorem names"
   4.212 -                       K.thy_decl (thm_maps >> Toplevel.theory);
   4.213 -   OuterSyntax.command "const_renames"
   4.214 +                       Keyword.thy_decl (thm_maps >> Toplevel.theory);
   4.215 +   Outer_Syntax.command "const_renames"
   4.216                         "Rename HOL4 const names"
   4.217 -                       K.thy_decl (const_renames >> Toplevel.theory);
   4.218 -   OuterSyntax.command "const_moves"
   4.219 +                       Keyword.thy_decl (const_renames >> Toplevel.theory);
   4.220 +   Outer_Syntax.command "const_moves"
   4.221                         "Rename HOL4 const names to other HOL4 constants"
   4.222 -                       K.thy_decl (const_moves >> Toplevel.theory);
   4.223 -   OuterSyntax.command "const_maps"
   4.224 +                       Keyword.thy_decl (const_moves >> Toplevel.theory);
   4.225 +   Outer_Syntax.command "const_maps"
   4.226                         "Map HOL4 const names to existing Isabelle/HOL const names"
   4.227 -                       K.thy_decl (const_maps >> Toplevel.theory));
   4.228 +                       Keyword.thy_decl (const_maps >> Toplevel.theory));
   4.229  
   4.230  end
   4.231 -
   4.232 -end
     5.1 --- a/src/HOL/Import/proof_kernel.ML	Mon May 17 15:11:25 2010 +0200
     5.2 +++ b/src/HOL/Import/proof_kernel.ML	Mon May 17 23:54:15 2010 +0200
     5.3 @@ -189,7 +189,7 @@
     5.4    else Delimfix (Syntax.escape c)
     5.5  
     5.6  fun quotename c =
     5.7 -  if Syntax.is_identifier c andalso not (OuterKeyword.is_keyword c) then c else quote c
     5.8 +  if Syntax.is_identifier c andalso not (Keyword.is_keyword c) then c else quote c
     5.9  
    5.10  fun simple_smart_string_of_cterm ct =
    5.11      let
     6.1 --- a/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Mon May 17 15:11:25 2010 +0200
     6.2 +++ b/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Mon May 17 23:54:15 2010 +0200
     6.3 @@ -144,11 +144,11 @@
     6.4  
     6.5  val setup =
     6.6    Method.setup @{binding sos}
     6.7 -    (Scan.lift (Scan.option OuterParse.xname)
     6.8 +    (Scan.lift (Scan.option Parse.xname)
     6.9        >> (sos_solver print_cert o Sum_Of_Squares.Prover o call_solver))
    6.10      "prove universal problems over the reals using sums of squares" #>
    6.11    Method.setup @{binding sos_cert}
    6.12 -    (Scan.lift OuterParse.string
    6.13 +    (Scan.lift Parse.string
    6.14        >> (fn cert => fn ctxt =>
    6.15          sos_solver ignore
    6.16            (Sum_Of_Squares.Certificate (PositivstellensatzTools.cert_to_pss_tree ctxt cert)) ctxt))
     7.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon May 17 15:11:25 2010 +0200
     7.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon May 17 23:54:15 2010 +0200
     7.3 @@ -330,7 +330,7 @@
     7.4  
     7.5  fun thms_of_name ctxt name =
     7.6    let
     7.7 -    val lex = OuterKeyword.get_lexicons
     7.8 +    val lex = Keyword.get_lexicons
     7.9      val get = maps (ProofContext.get_fact ctxt o fst)
    7.10    in
    7.11      Source.of_string name
     8.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Mon May 17 15:11:25 2010 +0200
     8.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Mon May 17 23:54:15 2010 +0200
     8.3 @@ -1004,10 +1004,10 @@
     8.4  
     8.5  
     8.6  (* syntax und parsing *)
     8.7 -structure P = OuterParse and K = OuterKeyword;
     8.8 +structure P = Parse and K = Keyword;
     8.9  
    8.10  val _ =
    8.11 -  OuterSyntax.command "atom_decl" "Declare new kinds of atoms" K.thy_decl
    8.12 -    (Scan.repeat1 P.name >> (Toplevel.theory o create_nom_typedecls));
    8.13 +  Outer_Syntax.command "atom_decl" "declare new kinds of atoms" Keyword.thy_decl
    8.14 +    (Scan.repeat1 Parse.name >> (Toplevel.theory o create_nom_typedecls));
    8.15  
    8.16  end;
     9.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Mon May 17 15:11:25 2010 +0200
     9.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Mon May 17 23:54:15 2010 +0200
     9.3 @@ -2076,11 +2076,10 @@
     9.4  
     9.5  (* FIXME: The following stuff should be exported by Datatype *)
     9.6  
     9.7 -local structure P = OuterParse and K = OuterKeyword in
     9.8 -
     9.9  val datatype_decl =
    9.10 -  Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_mixfix --
    9.11 -    (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
    9.12 +  Scan.option (Parse.$$$ "(" |-- Parse.name --| Parse.$$$ ")") --
    9.13 +    Parse.type_args -- Parse.name -- Parse.opt_mixfix --
    9.14 +    (Parse.$$$ "=" |-- Parse.enum1 "|" (Parse.name -- Scan.repeat Parse.typ -- Parse.opt_mixfix));
    9.15  
    9.16  fun mk_datatype args =
    9.17    let
    9.18 @@ -2090,9 +2089,7 @@
    9.19    in add_nominal_datatype Datatype.default_config names specs end;
    9.20  
    9.21  val _ =
    9.22 -  OuterSyntax.command "nominal_datatype" "define inductive datatypes" K.thy_decl
    9.23 -    (P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
    9.24 -
    9.25 -end;
    9.26 +  Outer_Syntax.command "nominal_datatype" "define inductive datatypes" Keyword.thy_decl
    9.27 +    (Parse.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
    9.28  
    9.29  end
    10.1 --- a/src/HOL/Nominal/nominal_induct.ML	Mon May 17 15:11:25 2010 +0200
    10.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Mon May 17 23:54:15 2010 +0200
    10.3 @@ -138,8 +138,6 @@
    10.4  
    10.5  local
    10.6  
    10.7 -structure P = OuterParse;
    10.8 -
    10.9  val avoidingN = "avoiding";
   10.10  val fixingN = "arbitrary";  (* to be consistent with induct; hopefully this changes again *)
   10.11  val ruleN = "rule";
   10.12 @@ -165,14 +163,14 @@
   10.13    Scan.repeat (unless_more_args free)) [];
   10.14  
   10.15  val fixing = Scan.optional (Scan.lift (Args.$$$ fixingN -- Args.colon) |--
   10.16 -  P.and_list' (Scan.repeat (unless_more_args free))) [];
   10.17 +  Parse.and_list' (Scan.repeat (unless_more_args free))) [];
   10.18  
   10.19  val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thms;
   10.20  
   10.21  in
   10.22  
   10.23  val nominal_induct_method =
   10.24 -  Args.mode Induct.no_simpN -- (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
   10.25 +  Args.mode Induct.no_simpN -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
   10.26    avoiding -- fixing -- rule_spec) >>
   10.27    (fn (no_simp, (((x, y), z), w)) => fn ctxt =>
   10.28      RAW_METHOD_CASES (fn facts =>
    11.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Mon May 17 15:11:25 2010 +0200
    11.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Mon May 17 23:54:15 2010 +0200
    11.3 @@ -672,23 +672,20 @@
    11.4  
    11.5  (* outer syntax *)
    11.6  
    11.7 -local structure P = OuterParse and K = OuterKeyword in
    11.8 -
    11.9 -val _ = OuterKeyword.keyword "avoids";
   11.10 +val _ = Keyword.keyword "avoids";
   11.11  
   11.12  val _ =
   11.13 -  OuterSyntax.local_theory_to_proof "nominal_inductive"
   11.14 -    "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal
   11.15 -    (P.xname -- Scan.optional (P.$$$ "avoids" |-- P.and_list1 (P.name --
   11.16 -      (P.$$$ ":" |-- Scan.repeat1 P.name))) [] >> (fn (name, avoids) =>
   11.17 +  Outer_Syntax.local_theory_to_proof "nominal_inductive"
   11.18 +    "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes"
   11.19 +    Keyword.thy_goal
   11.20 +    (Parse.xname -- Scan.optional (Parse.$$$ "avoids" |-- Parse.and_list1 (Parse.name --
   11.21 +      (Parse.$$$ ":" |-- Scan.repeat1 Parse.name))) [] >> (fn (name, avoids) =>
   11.22          prove_strong_ind name avoids));
   11.23  
   11.24  val _ =
   11.25 -  OuterSyntax.local_theory "equivariance"
   11.26 -    "prove equivariance for inductive predicate involving nominal datatypes" K.thy_decl
   11.27 -    (P.xname -- Scan.optional (P.$$$ "[" |-- P.list1 P.name --| P.$$$ "]") [] >>
   11.28 +  Outer_Syntax.local_theory "equivariance"
   11.29 +    "prove equivariance for inductive predicate involving nominal datatypes" Keyword.thy_decl
   11.30 +    (Parse.xname -- Scan.optional (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]") [] >>
   11.31        (fn (name, atoms) => prove_eqvt name atoms));
   11.32  
   11.33 -end;
   11.34 -
   11.35  end
    12.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Mon May 17 15:11:25 2010 +0200
    12.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Mon May 17 23:54:15 2010 +0200
    12.3 @@ -485,17 +485,14 @@
    12.4  
    12.5  (* outer syntax *)
    12.6  
    12.7 -local structure P = OuterParse and K = OuterKeyword in
    12.8 -
    12.9  val _ =
   12.10 -  OuterSyntax.local_theory_to_proof "nominal_inductive2"
   12.11 -    "prove strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal
   12.12 -    (P.xname -- 
   12.13 -     Scan.option (P.$$$ "(" |-- P.!!! (P.name --| P.$$$ ")")) --
   12.14 -     (Scan.optional (P.$$$ "avoids" |-- P.enum1 "|" (P.name --
   12.15 -      (P.$$$ ":" |-- P.and_list1 P.term))) []) >> (fn ((name, rule_name), avoids) =>
   12.16 +  Outer_Syntax.local_theory_to_proof "nominal_inductive2"
   12.17 +    "prove strong induction theorem for inductive predicate involving nominal datatypes"
   12.18 +    Keyword.thy_goal
   12.19 +    (Parse.xname -- 
   12.20 +     Scan.option (Parse.$$$ "(" |-- Parse.!!! (Parse.name --| Parse.$$$ ")")) --
   12.21 +     (Scan.optional (Parse.$$$ "avoids" |-- Parse.enum1 "|" (Parse.name --
   12.22 +      (Parse.$$$ ":" |-- Parse.and_list1 Parse.term))) []) >> (fn ((name, rule_name), avoids) =>
   12.23          prove_strong_ind name rule_name avoids));
   12.24  
   12.25 -end;
   12.26 -
   12.27  end
    13.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Mon May 17 15:11:25 2010 +0200
    13.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Mon May 17 23:54:15 2010 +0200
    13.3 @@ -393,28 +393,24 @@
    13.4  
    13.5  (* outer syntax *)
    13.6  
    13.7 -local structure P = OuterParse in
    13.8 -
    13.9 -val freshness_context = P.reserved "freshness_context";
   13.10 -val invariant = P.reserved "invariant";
   13.11 +val freshness_context = Parse.reserved "freshness_context";
   13.12 +val invariant = Parse.reserved "invariant";
   13.13  
   13.14 -fun unless_flag scan = Scan.unless ((freshness_context || invariant) -- P.$$$ ":") scan;
   13.15 +fun unless_flag scan = Scan.unless ((freshness_context || invariant) -- Parse.$$$ ":") scan;
   13.16  
   13.17 -val parser1 = (freshness_context -- P.$$$ ":") |-- unless_flag P.term >> SOME;
   13.18 -val parser2 = (invariant -- P.$$$ ":") |--
   13.19 -    (Scan.repeat1 (unless_flag P.term) >> SOME) -- Scan.optional parser1 NONE ||
   13.20 +val parser1 = (freshness_context -- Parse.$$$ ":") |-- unless_flag Parse.term >> SOME;
   13.21 +val parser2 = (invariant -- Parse.$$$ ":") |--
   13.22 +    (Scan.repeat1 (unless_flag Parse.term) >> SOME) -- Scan.optional parser1 NONE ||
   13.23    (parser1 >> pair NONE);
   13.24  val options =
   13.25 -  Scan.optional (P.$$$ "(" |-- P.!!! (parser2 --| P.$$$ ")")) (NONE, NONE);
   13.26 +  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (parser2 --| Parse.$$$ ")")) (NONE, NONE);
   13.27  
   13.28  val _ =
   13.29 -  OuterSyntax.local_theory_to_proof "nominal_primrec"
   13.30 -    "define primitive recursive functions on nominal datatypes" OuterKeyword.thy_goal
   13.31 -    (options -- P.fixes -- P.for_fixes -- Parse_Spec.where_alt_specs
   13.32 +  Outer_Syntax.local_theory_to_proof "nominal_primrec"
   13.33 +    "define primitive recursive functions on nominal datatypes" Keyword.thy_goal
   13.34 +    (options -- Parse.fixes -- Parse.for_fixes -- Parse_Spec.where_alt_specs
   13.35        >> (fn ((((invs, fctxt), fixes), params), specs) =>
   13.36          add_primrec_cmd invs fctxt fixes params specs));
   13.37  
   13.38  end;
   13.39  
   13.40 -end;
   13.41 -
    14.1 --- a/src/HOL/Orderings.thy	Mon May 17 15:11:25 2010 +0200
    14.2 +++ b/src/HOL/Orderings.thy	Mon May 17 23:54:15 2010 +0200
    14.3 @@ -422,8 +422,8 @@
    14.4  (** Diagnostic command **)
    14.5  
    14.6  val _ =
    14.7 -  OuterSyntax.improper_command "print_orders"
    14.8 -    "print order structures available to transitivity reasoner" OuterKeyword.diag
    14.9 +  Outer_Syntax.improper_command "print_orders"
   14.10 +    "print order structures available to transitivity reasoner" Keyword.diag
   14.11      (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
   14.12          Toplevel.keep (print_structures o Toplevel.context_of)));
   14.13  
    15.1 --- a/src/HOL/Statespace/state_space.ML	Mon May 17 15:11:25 2010 +0200
    15.2 +++ b/src/HOL/Statespace/state_space.ML	Mon May 17 23:54:15 2010 +0200
    15.3 @@ -667,37 +667,33 @@
    15.4  
    15.5  (*** outer syntax *)
    15.6  
    15.7 -local structure P = OuterParse and K = OuterKeyword in
    15.8 -
    15.9  val type_insts =
   15.10 -  P.typ >> single ||
   15.11 -  P.$$$ "(" |-- P.!!! (P.list1 P.typ --| P.$$$ ")")
   15.12 +  Parse.typ >> single ||
   15.13 +  Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.typ --| Parse.$$$ ")")
   15.14  
   15.15 -val comp = P.name -- (P.$$$ "::" |-- P.!!! P.typ);
   15.16 +val comp = Parse.name -- (Parse.$$$ "::" |-- Parse.!!! Parse.typ);
   15.17  fun plus1_unless test scan =
   15.18 -  scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
   15.19 +  scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan));
   15.20  
   15.21 -val mapsto = P.$$$ "=";
   15.22 -val rename = P.name -- (mapsto |-- P.name);
   15.23 -val renames =  Scan.optional (P.$$$ "[" |-- P.!!! (P.list1 rename --| P.$$$ "]")) [];
   15.24 +val mapsto = Parse.$$$ "=";
   15.25 +val rename = Parse.name -- (mapsto |-- Parse.name);
   15.26 +val renames = Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.list1 rename --| Parse.$$$ "]")) [];
   15.27  
   15.28  
   15.29 -val parent = ((type_insts -- P.xname) || (P.xname >> pair [])) -- renames
   15.30 +val parent = ((type_insts -- Parse.xname) || (Parse.xname >> pair [])) -- renames
   15.31               >> (fn ((insts,name),renames) => (insts,name,renames))
   15.32  
   15.33  
   15.34  val statespace_decl =
   15.35 -   P.type_args -- P.name --
   15.36 -    (P.$$$ "=" |--
   15.37 +   Parse.type_args -- Parse.name --
   15.38 +    (Parse.$$$ "=" |--
   15.39       ((Scan.repeat1 comp >> pair []) ||
   15.40        (plus1_unless comp parent --
   15.41 -        Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 comp)) [])))
   15.42 +        Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 comp)) [])))
   15.43  
   15.44  val statespace_command =
   15.45 -  OuterSyntax.command "statespace" "define state space" K.thy_decl
   15.46 +  Outer_Syntax.command "statespace" "define state space" Keyword.thy_decl
   15.47    (statespace_decl >> (fn ((args,name),(parents,comps)) =>
   15.48                             Toplevel.theory (define_statespace args name parents comps)))
   15.49  
   15.50 -end;
   15.51 -
   15.52  end;
   15.53 \ No newline at end of file
    16.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Mon May 17 15:11:25 2010 +0200
    16.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Mon May 17 23:54:15 2010 +0200
    16.3 @@ -721,8 +721,6 @@
    16.4  
    16.5  local
    16.6  
    16.7 -structure P = OuterParse and K = OuterKeyword
    16.8 -
    16.9  fun prep_datatype_decls args =
   16.10    let
   16.11      val names = map
   16.12 @@ -732,15 +730,16 @@
   16.13    in (names, specs) end;
   16.14  
   16.15  val parse_datatype_decl =
   16.16 -  (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_mixfix --
   16.17 -    (P.$$$ "=" |-- P.enum1 "|" (P.binding -- Scan.repeat P.typ -- P.opt_mixfix)));
   16.18 +  (Scan.option (Parse.$$$ "(" |-- Parse.name --| Parse.$$$ ")") --
   16.19 +    Parse.type_args -- Parse.binding -- Parse.opt_mixfix --
   16.20 +    (Parse.$$$ "=" |-- Parse.enum1 "|" (Parse.binding -- Scan.repeat Parse.typ -- Parse.opt_mixfix)));
   16.21  
   16.22 -val parse_datatype_decls = P.and_list1 parse_datatype_decl >> prep_datatype_decls;
   16.23 +val parse_datatype_decls = Parse.and_list1 parse_datatype_decl >> prep_datatype_decls;
   16.24  
   16.25  in
   16.26  
   16.27  val _ =
   16.28 -  OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl
   16.29 +  Outer_Syntax.command "datatype" "define inductive datatypes" Keyword.thy_decl
   16.30      (parse_datatype_decls >> (fn (names, specs) => Toplevel.theory (datatype_cmd names specs)));
   16.31  
   16.32  end;
    17.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Mon May 17 15:11:25 2010 +0200
    17.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Mon May 17 23:54:15 2010 +0200
    17.3 @@ -455,18 +455,11 @@
    17.4  
    17.5  (* outer syntax *)
    17.6  
    17.7 -local
    17.8 -
    17.9 -structure P = OuterParse and K = OuterKeyword
   17.10 -
   17.11 -in
   17.12 -
   17.13  val _ =
   17.14 -  OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_goal
   17.15 -    (Scan.option (P.$$$ "(" |-- Scan.repeat1 P.name --| P.$$$ ")") -- Scan.repeat1 P.term
   17.16 -      >> (fn (alt_names, ts) => Toplevel.print
   17.17 -           o Toplevel.theory_to_proof (rep_datatype_cmd alt_names ts)));
   17.18 +  Outer_Syntax.command "rep_datatype" "represent existing types inductively" Keyword.thy_goal
   17.19 +    (Scan.option (Parse.$$$ "(" |-- Scan.repeat1 Parse.name --| Parse.$$$ ")") --
   17.20 +      Scan.repeat1 Parse.term
   17.21 +      >> (fn (alt_names, ts) =>
   17.22 +        Toplevel.print o Toplevel.theory_to_proof (rep_datatype_cmd alt_names ts)));
   17.23  
   17.24  end;
   17.25 -
   17.26 -end;
    18.1 --- a/src/HOL/Tools/Function/fun.ML	Mon May 17 15:11:25 2010 +0200
    18.2 +++ b/src/HOL/Tools/Function/fun.ML	Mon May 17 23:54:15 2010 +0200
    18.3 @@ -159,13 +159,10 @@
    18.4  
    18.5  
    18.6  
    18.7 -local structure P = OuterParse and K = OuterKeyword in
    18.8 -
    18.9  val _ =
   18.10 -  OuterSyntax.local_theory "fun" "define general recursive functions (short version)" K.thy_decl
   18.11 +  Outer_Syntax.local_theory "fun" "define general recursive functions (short version)"
   18.12 +  Keyword.thy_decl
   18.13    (function_parser fun_config
   18.14 -     >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config));
   18.15 +     >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config))
   18.16  
   18.17  end
   18.18 -
   18.19 -end
    19.1 --- a/src/HOL/Tools/Function/function.ML	Mon May 17 15:11:25 2010 +0200
    19.2 +++ b/src/HOL/Tools/Function/function.ML	Mon May 17 23:54:15 2010 +0200
    19.3 @@ -274,20 +274,19 @@
    19.4  fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t
    19.5    |> the_single |> snd
    19.6  
    19.7 +
    19.8  (* outer syntax *)
    19.9  
   19.10 -local structure P = OuterParse and K = OuterKeyword in
   19.11 -
   19.12  val _ =
   19.13 -  OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal
   19.14 +  Outer_Syntax.local_theory_to_proof "function" "define general recursive functions"
   19.15 +  Keyword.thy_goal
   19.16    (function_parser default_config
   19.17       >> (fn ((config, fixes), statements) => function_cmd fixes statements config))
   19.18  
   19.19  val _ =
   19.20 -  OuterSyntax.local_theory_to_proof "termination" "prove termination of a recursive function" K.thy_goal
   19.21 -  (Scan.option P.term >> termination_cmd)
   19.22 -
   19.23 -end
   19.24 +  Outer_Syntax.local_theory_to_proof "termination" "prove termination of a recursive function"
   19.25 +  Keyword.thy_goal
   19.26 +  (Scan.option Parse.term >> termination_cmd)
   19.27  
   19.28  
   19.29  end
    20.1 --- a/src/HOL/Tools/Function/function_common.ML	Mon May 17 15:11:25 2010 +0200
    20.2 +++ b/src/HOL/Tools/Function/function_common.ML	Mon May 17 23:54:15 2010 +0200
    20.3 @@ -341,21 +341,19 @@
    20.4  
    20.5  
    20.6  local
    20.7 -  structure P = OuterParse and K = OuterKeyword
    20.8 -
    20.9 -  val option_parser = P.group "option"
   20.10 -    ((P.reserved "sequential" >> K Sequential)
   20.11 -     || ((P.reserved "default" |-- P.term) >> Default)
   20.12 -     || (P.reserved "domintros" >> K DomIntros)
   20.13 -     || (P.reserved "no_partials" >> K No_Partials)
   20.14 -     || (P.reserved "tailrec" >> K Tailrec))
   20.15 +  val option_parser = Parse.group "option"
   20.16 +    ((Parse.reserved "sequential" >> K Sequential)
   20.17 +     || ((Parse.reserved "default" |-- Parse.term) >> Default)
   20.18 +     || (Parse.reserved "domintros" >> K DomIntros)
   20.19 +     || (Parse.reserved "no_partials" >> K No_Partials)
   20.20 +     || (Parse.reserved "tailrec" >> K Tailrec))
   20.21  
   20.22    fun config_parser default =
   20.23 -    (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 option_parser) --| P.$$$ ")") [])
   20.24 +    (Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 option_parser) --| Parse.$$$ ")") [])
   20.25       >> (fn opts => fold apply_opt opts default)
   20.26  in
   20.27    fun function_parser default_cfg =
   20.28 -      config_parser default_cfg -- P.fixes -- Parse_Spec.where_alt_specs
   20.29 +      config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs
   20.30  end
   20.31  
   20.32  
    21.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon May 17 15:11:25 2010 +0200
    21.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon May 17 23:54:15 2010 +0200
    21.3 @@ -24,8 +24,6 @@
    21.4  open Nitpick_Nut
    21.5  open Nitpick
    21.6  
    21.7 -structure K = OuterKeyword and P = OuterParse
    21.8 -
    21.9  val auto = Unsynchronized.ref false;
   21.10  
   21.11  val _ =
   21.12 @@ -289,14 +287,14 @@
   21.13    extract_params (ProofContext.init_global thy) false (default_raw_params thy)
   21.14    o map (apsnd single)
   21.15  
   21.16 -val parse_key = Scan.repeat1 P.typ_group >> space_implode " "
   21.17 +val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
   21.18  val parse_value =
   21.19 -  Scan.repeat1 (P.minus >> single
   21.20 -                || Scan.repeat1 (Scan.unless P.minus P.name)
   21.21 -                || P.$$$ "," |-- P.number >> prefix "," >> single) >> flat
   21.22 -val parse_param = parse_key -- Scan.optional (P.$$$ "=" |-- parse_value) []
   21.23 +  Scan.repeat1 (Parse.minus >> single
   21.24 +                || Scan.repeat1 (Scan.unless Parse.minus Parse.name)
   21.25 +                || Parse.$$$ "," |-- Parse.number >> prefix "," >> single) >> flat
   21.26 +val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
   21.27  val parse_params =
   21.28 -  Scan.optional (P.$$$ "[" |-- P.list parse_param --| P.$$$ "]") []
   21.29 +  Scan.optional (Parse.$$$ "[" |-- Parse.list parse_param --| Parse.$$$ "]") []
   21.30  
   21.31  fun handle_exceptions ctxt f x =
   21.32    f x
   21.33 @@ -375,15 +373,15 @@
   21.34                                        |> sort_strings |> cat_lines)))))
   21.35  
   21.36  val parse_nitpick_command =
   21.37 -  (parse_params -- Scan.optional P.nat 1) #>> nitpick_trans
   21.38 +  (parse_params -- Scan.optional Parse.nat 1) #>> nitpick_trans
   21.39  val parse_nitpick_params_command = parse_params #>> nitpick_params_trans
   21.40  
   21.41 -val _ = OuterSyntax.improper_command "nitpick"
   21.42 +val _ = Outer_Syntax.improper_command "nitpick"
   21.43              "try to find a counterexample for a given subgoal using Nitpick"
   21.44 -            K.diag parse_nitpick_command
   21.45 -val _ = OuterSyntax.command "nitpick_params"
   21.46 +            Keyword.diag parse_nitpick_command
   21.47 +val _ = Outer_Syntax.command "nitpick_params"
   21.48              "set and display the default parameters for Nitpick"
   21.49 -            K.thy_decl parse_nitpick_params_command
   21.50 +            Keyword.thy_decl parse_nitpick_params_command
   21.51  
   21.52  fun auto_nitpick state =
   21.53    if not (!auto) then (false, state) else pick_nits [] true 1 0 state
    22.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon May 17 15:11:25 2010 +0200
    22.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon May 17 23:54:15 2010 +0200
    22.3 @@ -192,8 +192,6 @@
    22.4  
    22.5  val setup = Predicate_Compile_Core.setup
    22.6  
    22.7 -local structure P = OuterParse
    22.8 -in
    22.9  
   22.10  (* Parser for mode annotations *)
   22.11  
   22.12 @@ -207,15 +205,15 @@
   22.13    (parse_mode_tuple_expr --| Args.$$$ "=>" -- parse_mode_expr >> Fun || parse_mode_tuple_expr) xs
   22.14  
   22.15  val mode_and_opt_proposal = parse_mode_expr --
   22.16 -  Scan.optional (Args.$$$ "as" |-- P.xname >> SOME) NONE
   22.17 +  Scan.optional (Args.$$$ "as" |-- Parse.xname >> SOME) NONE
   22.18  
   22.19  val opt_modes =
   22.20 -  Scan.optional (P.$$$ "(" |-- Args.$$$ "modes" |-- P.$$$ ":" |--
   22.21 -    P.enum "," mode_and_opt_proposal --| P.$$$ ")" >> SOME) NONE
   22.22 +  Scan.optional (Parse.$$$ "(" |-- Args.$$$ "modes" |-- Parse.$$$ ":" |--
   22.23 +    Parse.enum "," mode_and_opt_proposal --| Parse.$$$ ")" >> SOME) NONE
   22.24  
   22.25  val opt_expected_modes =
   22.26 -  Scan.optional (P.$$$ "(" |-- Args.$$$ "expected_modes" |-- P.$$$ ":" |--
   22.27 -    P.enum "," parse_mode_expr --| P.$$$ ")" >> SOME) NONE
   22.28 +  Scan.optional (Parse.$$$ "(" |-- Args.$$$ "expected_modes" |-- Parse.$$$ ":" |--
   22.29 +    Parse.enum "," parse_mode_expr --| Parse.$$$ ")" >> SOME) NONE
   22.30  
   22.31  (* Parser for options *)
   22.32  
   22.33 @@ -224,46 +222,46 @@
   22.34      val scan_bool_option = foldl1 (op ||) (map Args.$$$ bool_options)
   22.35      val scan_compilation = foldl1 (op ||) (map (fn (s, c) => Args.$$$ s >> K c) compilation_names)
   22.36    in
   22.37 -    Scan.optional (P.$$$ "[" |-- Scan.optional scan_compilation Pred
   22.38 -      -- P.enum "," scan_bool_option --| P.$$$ "]")
   22.39 +    Scan.optional (Parse.$$$ "[" |-- Scan.optional scan_compilation Pred
   22.40 +      -- Parse.enum "," scan_bool_option --| Parse.$$$ "]")
   22.41        (Pred, [])
   22.42    end
   22.43  
   22.44 -val opt_print_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
   22.45 +val opt_print_modes =
   22.46 +  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
   22.47  
   22.48 -val opt_mode = (P.$$$ "_" >> K NONE) || (parse_mode_expr >> SOME)
   22.49 +val opt_mode = (Parse.$$$ "_" >> K NONE) || (parse_mode_expr >> SOME)
   22.50  
   22.51 -val opt_param_modes = Scan.optional (P.$$$ "[" |-- Args.$$$ "mode" |-- P.$$$ ":" |--
   22.52 -  P.enum ", " opt_mode --| P.$$$ "]" >> SOME) NONE
   22.53 +val opt_param_modes = Scan.optional (Parse.$$$ "[" |-- Args.$$$ "mode" |-- Parse.$$$ ":" |--
   22.54 +  Parse.enum ", " opt_mode --| Parse.$$$ "]" >> SOME) NONE
   22.55  
   22.56  val stats = Scan.optional (Args.$$$ "stats" >> K true) false
   22.57  
   22.58  val value_options =
   22.59    let
   22.60 -    val expected_values = Scan.optional (Args.$$$ "expected" |-- P.term >> SOME) NONE
   22.61 +    val expected_values = Scan.optional (Args.$$$ "expected" |-- Parse.term >> SOME) NONE
   22.62      val scan_compilation =
   22.63        Scan.optional
   22.64          (foldl1 (op ||)
   22.65 -          (map (fn (s, c) => Args.$$$ s -- P.enum "," P.int >> (fn (_, ps) => (c, ps)))
   22.66 +          (map (fn (s, c) => Args.$$$ s -- Parse.enum "," Parse.int >> (fn (_, ps) => (c, ps)))
   22.67              compilation_names))
   22.68          (Pred, [])
   22.69    in
   22.70 -    Scan.optional (P.$$$ "[" |-- (expected_values -- stats) -- scan_compilation --| P.$$$ "]")
   22.71 +    Scan.optional
   22.72 +      (Parse.$$$ "[" |-- (expected_values -- stats) -- scan_compilation --| Parse.$$$ "]")
   22.73        ((NONE, false), (Pred, []))
   22.74    end
   22.75  
   22.76  (* code_pred command and values command *)
   22.77  
   22.78 -val _ = OuterSyntax.local_theory_to_proof "code_pred"
   22.79 +val _ = Outer_Syntax.local_theory_to_proof "code_pred"
   22.80    "prove equations for predicate specified by intro/elim rules"
   22.81 -  OuterKeyword.thy_goal
   22.82 -  (opt_expected_modes -- opt_modes -- scan_options -- P.term_group >> code_pred_cmd)
   22.83 +  Keyword.thy_goal
   22.84 +  (opt_expected_modes -- opt_modes -- scan_options -- Parse.term_group >> code_pred_cmd)
   22.85  
   22.86 -val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag
   22.87 -  (opt_print_modes -- opt_param_modes -- value_options -- Scan.optional P.nat ~1 -- P.term
   22.88 +val _ = Outer_Syntax.improper_command "values" "enumerate and print comprehensions" Keyword.diag
   22.89 +  (opt_print_modes -- opt_param_modes -- value_options -- Scan.optional Parse.nat ~1 -- Parse.term
   22.90      >> (fn ((((print_modes, param_modes), options), k), t) => Toplevel.keep
   22.91          (Predicate_Compile_Core.values_cmd print_modes param_modes options k t)));
   22.92  
   22.93  end
   22.94 -
   22.95 -end
    23.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Mon May 17 15:11:25 2010 +0200
    23.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Mon May 17 23:54:15 2010 +0200
    23.3 @@ -91,20 +91,15 @@
    23.4    quotient_def ((NONE, NoSyn), (Attrib.empty_binding,
    23.5      (Quotient_Term.quotient_lift_const qtys (b, t) ctxt, t))) ctxt
    23.6  
    23.7 -local
    23.8 -  structure P = OuterParse;
    23.9 -in
   23.10 -
   23.11 -val quotdef_decl = (P.binding >> SOME) -- P.opt_mixfix' --| P.$$$ "where"
   23.12 +val quotdef_decl = (Parse.binding >> SOME) -- Parse.opt_mixfix' --| Parse.$$$ "where"
   23.13  
   23.14  val quotdef_parser =
   23.15    Scan.optional quotdef_decl (NONE, NoSyn) -- 
   23.16 -    P.!!! (Parse_Spec.opt_thm_name ":" -- (P.term --| P.$$$ "is" -- P.term))
   23.17 -end
   23.18 +    Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| Parse.$$$ "is" -- Parse.term))
   23.19  
   23.20  val _ =
   23.21 -  OuterSyntax.local_theory "quotient_definition"
   23.22 +  Outer_Syntax.local_theory "quotient_definition"
   23.23      "definition for constants over the quotient type"
   23.24 -      OuterKeyword.thy_decl (quotdef_parser >> (snd oo quotdef_cmd))
   23.25 +      Keyword.thy_decl (quotdef_parser >> (snd oo quotdef_cmd))
   23.26  
   23.27  end; (* structure *)
    24.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Mon May 17 15:11:25 2010 +0200
    24.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Mon May 17 23:54:15 2010 +0200
    24.3 @@ -91,9 +91,9 @@
    24.4  
    24.5  val maps_attr_parser =
    24.6    Args.context -- Scan.lift
    24.7 -    ((Args.name --| OuterParse.$$$ "=") --
    24.8 -      (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," --
    24.9 -        Args.name --| OuterParse.$$$ ")"))
   24.10 +    ((Args.name --| Parse.$$$ "=") --
   24.11 +      (Parse.$$$ "(" |-- Args.name --| Parse.$$$ "," --
   24.12 +        Args.name --| Parse.$$$ ")"))
   24.13  
   24.14  val _ = Context.>> (Context.map_theory
   24.15    (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute)
   24.16 @@ -278,8 +278,8 @@
   24.17  (* setup of the printing commands *)
   24.18  
   24.19  fun improper_command (pp_fn, cmd_name, descr_str) =
   24.20 -  OuterSyntax.improper_command cmd_name descr_str
   24.21 -    OuterKeyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of)))
   24.22 +  Outer_Syntax.improper_command cmd_name descr_str
   24.23 +    Keyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of)))
   24.24  
   24.25  val _ = map improper_command
   24.26    [(print_mapsinfo, "print_quotmaps", "prints out all map functions"),
    25.1 --- a/src/HOL/Tools/Quotient/quotient_typ.ML	Mon May 17 15:11:25 2010 +0200
    25.2 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Mon May 17 23:54:15 2010 +0200
    25.3 @@ -299,16 +299,16 @@
    25.4  end
    25.5  
    25.6  val quotspec_parser =
    25.7 -    OuterParse.and_list1
    25.8 -     ((OuterParse.type_args -- OuterParse.binding) --
    25.9 -        OuterParse.opt_mixfix -- (OuterParse.$$$ "=" |-- OuterParse.typ) --
   25.10 -         (OuterParse.$$$ "/" |-- OuterParse.term))
   25.11 +    Parse.and_list1
   25.12 +     ((Parse.type_args -- Parse.binding) --
   25.13 +        Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) --
   25.14 +         (Parse.$$$ "/" |-- Parse.term))
   25.15  
   25.16 -val _ = OuterKeyword.keyword "/"
   25.17 +val _ = Keyword.keyword "/"
   25.18  
   25.19  val _ =
   25.20 -    OuterSyntax.local_theory_to_proof "quotient_type"
   25.21 +    Outer_Syntax.local_theory_to_proof "quotient_type"
   25.22        "quotient type definitions (require equivalence proofs)"
   25.23 -         OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd)
   25.24 +         Keyword.thy_goal (quotspec_parser >> quotient_type_cmd)
   25.25  
   25.26  end; (* structure *)
    26.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Mon May 17 15:11:25 2010 +0200
    26.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Mon May 17 23:54:15 2010 +0200
    26.3 @@ -311,14 +311,14 @@
    26.4  
    26.5  val setup =
    26.6    Attrib.setup (Binding.name "smt_solver")
    26.7 -    (Scan.lift (OuterParse.$$$ "=" |-- Args.name) >>
    26.8 +    (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
    26.9        (Thm.declaration_attribute o K o select_solver))
   26.10      "SMT solver configuration" #>
   26.11    setup_timeout #>
   26.12    setup_trace #>
   26.13    setup_fixed_certificates #>
   26.14    Attrib.setup (Binding.name "smt_certificates")
   26.15 -    (Scan.lift (OuterParse.$$$ "=" |-- Args.name) >>
   26.16 +    (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
   26.17        (Thm.declaration_attribute o K o select_certificates))
   26.18      "SMT certificates" #>
   26.19    Method.setup (Binding.name "smt") smt_method
   26.20 @@ -353,9 +353,9 @@
   26.21        Pretty.big_list "Solver-specific settings:" infos])
   26.22    end
   26.23  
   26.24 -val _ = OuterSyntax.improper_command "smt_status"
   26.25 -  "Show the available SMT solvers and the currently selected solver."
   26.26 -  OuterKeyword.diag
   26.27 +val _ =
   26.28 +  Outer_Syntax.improper_command "smt_status"
   26.29 +    "show the available SMT solvers and the currently selected solver" Keyword.diag
   26.30      (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
   26.31        print_setup (Context.Proof (Toplevel.context_of state)))))
   26.32  
    27.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon May 17 15:11:25 2010 +0200
    27.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon May 17 23:54:15 2010 +0200
    27.3 @@ -24,8 +24,6 @@
    27.4  open ATP_Systems
    27.5  open Sledgehammer_Fact_Minimizer
    27.6  
    27.7 -structure K = OuterKeyword and P = OuterParse
    27.8 -
    27.9  (** Proof method used in Isar proofs **)
   27.10  
   27.11  val neg_clausify_setup =
   27.12 @@ -36,7 +34,7 @@
   27.13  (** Attribute for converting a theorem into clauses **)
   27.14  
   27.15  val parse_clausify_attribute : attribute context_parser =
   27.16 -  Scan.lift OuterParse.nat
   27.17 +  Scan.lift Parse.nat
   27.18    >> (fn i => Thm.rule_attribute (fn context => fn th =>
   27.19                    let val thy = Context.theory_of context in
   27.20                      Meson.make_meta_clause (nth (cnf_axiom thy th) i)
   27.21 @@ -321,13 +319,13 @@
   27.22                                 params |> map string_for_raw_param
   27.23                                        |> sort_strings |> cat_lines)))))
   27.24  
   27.25 -val parse_key = Scan.repeat1 P.typ_group >> space_implode " "
   27.26 -val parse_value = Scan.repeat1 P.xname
   27.27 -val parse_param = parse_key -- Scan.optional (P.$$$ "=" |-- parse_value) []
   27.28 -val parse_params = Scan.optional (Args.bracks (P.list parse_param)) []
   27.29 +val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
   27.30 +val parse_value = Scan.repeat1 Parse.xname
   27.31 +val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
   27.32 +val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
   27.33  val parse_fact_refs =
   27.34 -  Scan.repeat1 (Scan.unless (P.name -- Args.colon)
   27.35 -                            (P.xname -- Scan.option Attrib.thm_sel)
   27.36 +  Scan.repeat1 (Scan.unless (Parse.name -- Args.colon)
   27.37 +                            (Parse.xname -- Scan.option Attrib.thm_sel)
   27.38                  >> (fn (name, interval) =>
   27.39                         Facts.Named ((name, Position.none), interval)))
   27.40  val parse_relevance_chunk =
   27.41 @@ -340,18 +338,18 @@
   27.42                                >> merge_relevance_overrides))
   27.43                  (add_to_relevance_override [])
   27.44  val parse_sledgehammer_command =
   27.45 -  (Scan.optional P.short_ident runN -- parse_params -- parse_relevance_override
   27.46 -   -- Scan.option P.nat) #>> sledgehammer_trans
   27.47 +  (Scan.optional Parse.short_ident runN -- parse_params -- parse_relevance_override
   27.48 +   -- Scan.option Parse.nat) #>> sledgehammer_trans
   27.49  val parse_sledgehammer_params_command =
   27.50    parse_params #>> sledgehammer_params_trans
   27.51  
   27.52  val _ =
   27.53 -  OuterSyntax.improper_command sledgehammerN
   27.54 -      "search for first-order proof using automatic theorem provers" K.diag
   27.55 +  Outer_Syntax.improper_command sledgehammerN
   27.56 +      "search for first-order proof using automatic theorem provers" Keyword.diag
   27.57        parse_sledgehammer_command
   27.58  val _ =
   27.59 -  OuterSyntax.command sledgehammer_paramsN
   27.60 -      "set and display the default parameters for Sledgehammer" K.thy_decl
   27.61 +  Outer_Syntax.command sledgehammer_paramsN
   27.62 +      "set and display the default parameters for Sledgehammer" Keyword.thy_decl
   27.63        parse_sledgehammer_params_command
   27.64  
   27.65  val setup =
    28.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon May 17 15:11:25 2010 +0200
    28.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon May 17 23:54:15 2010 +0200
    28.3 @@ -102,7 +102,7 @@
    28.4    let val s = unyxml y in
    28.5      y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso
    28.6             not (is_long_identifier (perhaps (try (unprefix "?")) s))) orelse
    28.7 -           OuterKeyword.is_keyword s) ? quote
    28.8 +           Keyword.is_keyword s) ? quote
    28.9    end
   28.10  
   28.11  fun monomorphic_term subst t =
    29.1 --- a/src/HOL/Tools/choice_specification.ML	Mon May 17 15:11:25 2010 +0200
    29.2 +++ b/src/HOL/Tools/choice_specification.ML	Mon May 17 23:54:15 2010 +0200
    29.3 @@ -232,33 +232,28 @@
    29.4  
    29.5  (* outer syntax *)
    29.6  
    29.7 -local structure P = OuterParse and K = OuterKeyword in
    29.8 -
    29.9 -val opt_name = Scan.optional (P.name --| P.$$$ ":") ""
   29.10 -val opt_overloaded = P.opt_keyword "overloaded";
   29.11 +val opt_name = Scan.optional (Parse.name --| Parse.$$$ ":") ""
   29.12 +val opt_overloaded = Parse.opt_keyword "overloaded"
   29.13  
   29.14  val specification_decl =
   29.15 -  P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
   29.16 -          Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop)
   29.17 +  Parse.$$$ "(" |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| Parse.$$$ ")" --
   29.18 +          Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop)
   29.19  
   29.20  val _ =
   29.21 -  OuterSyntax.command "specification" "define constants by specification" K.thy_goal
   29.22 +  Outer_Syntax.command "specification" "define constants by specification" Keyword.thy_goal
   29.23      (specification_decl >> (fn (cos,alt_props) =>
   29.24                                 Toplevel.print o (Toplevel.theory_to_proof
   29.25                                                       (process_spec NONE cos alt_props))))
   29.26  
   29.27  val ax_specification_decl =
   29.28 -    P.name --
   29.29 -    (P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
   29.30 -           Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop))
   29.31 +    Parse.name --
   29.32 +    (Parse.$$$ "(" |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| Parse.$$$ ")" --
   29.33 +           Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop))
   29.34  
   29.35  val _ =
   29.36 -  OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal
   29.37 +  Outer_Syntax.command "ax_specification" "define constants by specification" Keyword.thy_goal
   29.38      (ax_specification_decl >> (fn (axname,(cos,alt_props)) =>
   29.39                                 Toplevel.print o (Toplevel.theory_to_proof
   29.40                                                       (process_spec (SOME axname) cos alt_props))))
   29.41  
   29.42  end
   29.43 -
   29.44 -
   29.45 -end
    30.1 --- a/src/HOL/Tools/inductive.ML	Mon May 17 15:11:25 2010 +0200
    30.2 +++ b/src/HOL/Tools/inductive.ML	Mon May 17 23:54:15 2010 +0200
    30.3 @@ -970,32 +970,28 @@
    30.4  
    30.5  (* outer syntax *)
    30.6  
    30.7 -local structure P = OuterParse and K = OuterKeyword in
    30.8 -
    30.9 -val _ = OuterKeyword.keyword "monos";
   30.10 +val _ = Keyword.keyword "monos";
   30.11  
   30.12  fun gen_ind_decl mk_def coind =
   30.13 -  P.fixes -- P.for_fixes --
   30.14 +  Parse.fixes -- Parse.for_fixes --
   30.15    Scan.optional Parse_Spec.where_alt_specs [] --
   30.16 -  Scan.optional (P.$$$ "monos" |-- P.!!! Parse_Spec.xthms1) []
   30.17 +  Scan.optional (Parse.$$$ "monos" |-- Parse.!!! Parse_Spec.xthms1) []
   30.18    >> (fn (((preds, params), specs), monos) =>
   30.19        (snd oo gen_add_inductive mk_def true coind preds params specs monos));
   30.20  
   30.21  val ind_decl = gen_ind_decl add_ind_def;
   30.22  
   30.23  val _ =
   30.24 -  OuterSyntax.local_theory' "inductive" "define inductive predicates" K.thy_decl
   30.25 +  Outer_Syntax.local_theory' "inductive" "define inductive predicates" Keyword.thy_decl
   30.26      (ind_decl false);
   30.27  
   30.28  val _ =
   30.29 -  OuterSyntax.local_theory' "coinductive" "define coinductive predicates" K.thy_decl
   30.30 +  Outer_Syntax.local_theory' "coinductive" "define coinductive predicates" Keyword.thy_decl
   30.31      (ind_decl true);
   30.32  
   30.33  val _ =
   30.34 -  OuterSyntax.local_theory "inductive_cases"
   30.35 -    "create simplified instances of elimination rules (improper)" K.thy_script
   30.36 -    (P.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
   30.37 +  Outer_Syntax.local_theory "inductive_cases"
   30.38 +    "create simplified instances of elimination rules (improper)" Keyword.thy_script
   30.39 +    (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
   30.40  
   30.41  end;
   30.42 -
   30.43 -end;
    31.1 --- a/src/HOL/Tools/inductive_codegen.ML	Mon May 17 15:11:25 2010 +0200
    31.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Mon May 17 23:54:15 2010 +0200
    31.3 @@ -775,7 +775,7 @@
    31.4    add_codegen "inductive" inductive_codegen #>
    31.5    Attrib.setup @{binding code_ind}
    31.6      (Scan.lift (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
    31.7 -      Scan.option (Args.$$$ "params" |-- Args.colon |-- OuterParse.nat) >> uncurry add))
    31.8 +      Scan.option (Args.$$$ "params" |-- Args.colon |-- Parse.nat) >> uncurry add))
    31.9      "introduction rules for executable predicates";
   31.10  
   31.11  (**** Quickcheck involving inductive predicates ****)
    32.1 --- a/src/HOL/Tools/inductive_set.ML	Mon May 17 15:11:25 2010 +0200
    32.2 +++ b/src/HOL/Tools/inductive_set.ML	Mon May 17 23:54:15 2010 +0200
    32.3 @@ -562,18 +562,14 @@
    32.4  
    32.5  (* outer syntax *)
    32.6  
    32.7 -local structure P = OuterParse and K = OuterKeyword in
    32.8 -
    32.9  val ind_set_decl = Inductive.gen_ind_decl add_ind_set_def;
   32.10  
   32.11  val _ =
   32.12 -  OuterSyntax.local_theory' "inductive_set" "define inductive sets" K.thy_decl
   32.13 +  Outer_Syntax.local_theory' "inductive_set" "define inductive sets" Keyword.thy_decl
   32.14      (ind_set_decl false);
   32.15  
   32.16  val _ =
   32.17 -  OuterSyntax.local_theory' "coinductive_set" "define coinductive sets" K.thy_decl
   32.18 +  Outer_Syntax.local_theory' "coinductive_set" "define coinductive sets" Keyword.thy_decl
   32.19      (ind_set_decl true);
   32.20  
   32.21  end;
   32.22 -
   32.23 -end;
    33.1 --- a/src/HOL/Tools/primrec.ML	Mon May 17 15:11:25 2010 +0200
    33.2 +++ b/src/HOL/Tools/primrec.ML	Mon May 17 23:54:15 2010 +0200
    33.3 @@ -307,29 +307,26 @@
    33.4  
    33.5  (* outer syntax *)
    33.6  
    33.7 -local structure P = OuterParse and K = OuterKeyword in
    33.8 -
    33.9  val opt_unchecked_name =
   33.10 -  Scan.optional (P.$$$ "(" |-- P.!!!
   33.11 -    (((P.$$$ "unchecked" >> K true) -- Scan.optional P.name "" ||
   33.12 -      P.name >> pair false) --| P.$$$ ")")) (false, "");
   33.13 +  Scan.optional (Parse.$$$ "(" |-- Parse.!!!
   33.14 +    (((Parse.$$$ "unchecked" >> K true) -- Scan.optional Parse.name "" ||
   33.15 +      Parse.name >> pair false) --| Parse.$$$ ")")) (false, "");
   33.16  
   33.17  val old_primrec_decl =
   33.18    opt_unchecked_name --
   33.19 -    Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop);
   33.20 +    Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop);
   33.21  
   33.22 -val primrec_decl = P.opt_target -- P.fixes -- Parse_Spec.where_alt_specs;
   33.23 +val primrec_decl = Parse.opt_target -- Parse.fixes -- Parse_Spec.where_alt_specs;
   33.24  
   33.25  val _ =
   33.26 -  OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
   33.27 +  Outer_Syntax.command "primrec" "define primitive recursive functions on datatypes"
   33.28 +  Keyword.thy_decl
   33.29      ((primrec_decl >> (fn ((opt_target, fixes), specs) =>
   33.30        Toplevel.local_theory opt_target (add_primrec_cmd fixes specs #> snd)))
   33.31      || (old_primrec_decl >> (fn ((unchecked, alt_name), eqns) =>
   33.32        Toplevel.theory (snd o
   33.33          (if unchecked then OldPrimrec.add_primrec_unchecked else OldPrimrec.add_primrec)
   33.34 -          alt_name (map P.triple_swap eqns) o
   33.35 +          alt_name (map Parse.triple_swap eqns) o
   33.36          tap (fn _ => legacy_feature "Old variant of 'primrec' command -- use new syntax instead")))));
   33.37  
   33.38  end;
   33.39 -
   33.40 -end;
    34.1 --- a/src/HOL/Tools/recdef.ML	Mon May 17 15:11:25 2010 +0200
    34.2 +++ b/src/HOL/Tools/recdef.ML	Mon May 17 23:54:15 2010 +0200
    34.3 @@ -289,40 +289,39 @@
    34.4  
    34.5  (* outer syntax *)
    34.6  
    34.7 -local structure P = OuterParse and K = OuterKeyword in
    34.8 -
    34.9 -val _ = List.app OuterKeyword.keyword ["permissive", "congs", "hints"];
   34.10 +val _ = List.app Keyword.keyword ["permissive", "congs", "hints"];
   34.11  
   34.12  val hints =
   34.13 -  P.$$$ "(" |-- P.!!! (P.position (P.$$$ "hints" -- Args.parse) --| P.$$$ ")") >> Args.src;
   34.14 +  Parse.$$$ "(" |--
   34.15 +    Parse.!!! (Parse.position (Parse.$$$ "hints" -- Args.parse) --| Parse.$$$ ")") >> Args.src;
   34.16  
   34.17  val recdef_decl =
   34.18 -  Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true --
   34.19 -  P.name -- P.term -- Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- P.prop)
   34.20 +  Scan.optional
   34.21 +    (Parse.$$$ "(" -- Parse.!!! (Parse.$$$ "permissive" -- Parse.$$$ ")") >> K false) true --
   34.22 +  Parse.name -- Parse.term -- Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)
   34.23      -- Scan.option hints
   34.24 -  >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
   34.25 +  >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map Parse.triple_swap eqs) src);
   34.26  
   34.27  val _ =
   34.28 -  OuterSyntax.command "recdef" "define general recursive functions (TFL)" K.thy_decl
   34.29 +  Outer_Syntax.command "recdef" "define general recursive functions (TFL)" Keyword.thy_decl
   34.30      (recdef_decl >> Toplevel.theory);
   34.31  
   34.32  
   34.33  val defer_recdef_decl =
   34.34 -  P.name -- Scan.repeat1 P.prop --
   34.35 -  Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (Parse_Spec.xthms1 --| P.$$$ ")")) []
   34.36 +  Parse.name -- Scan.repeat1 Parse.prop --
   34.37 +  Scan.optional
   34.38 +    (Parse.$$$ "(" |-- Parse.$$$ "congs" |-- Parse.!!! (Parse_Spec.xthms1 --| Parse.$$$ ")")) []
   34.39    >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
   34.40  
   34.41  val _ =
   34.42 -  OuterSyntax.command "defer_recdef" "defer general recursive functions (TFL)" K.thy_decl
   34.43 +  Outer_Syntax.command "defer_recdef" "defer general recursive functions (TFL)" Keyword.thy_decl
   34.44      (defer_recdef_decl >> Toplevel.theory);
   34.45  
   34.46  val _ =
   34.47 -  OuterSyntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
   34.48 -    K.thy_goal
   34.49 -    ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- P.xname --
   34.50 -        Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
   34.51 +  Outer_Syntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
   34.52 +    Keyword.thy_goal
   34.53 +    ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.xname --
   34.54 +        Scan.option (Parse.$$$ "(" |-- Parse.nat --| Parse.$$$ ")")
   34.55        >> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
   34.56  
   34.57  end;
   34.58 -
   34.59 -end;
    35.1 --- a/src/HOL/Tools/record.ML	Mon May 17 15:11:25 2010 +0200
    35.2 +++ b/src/HOL/Tools/record.ML	Mon May 17 23:54:15 2010 +0200
    35.3 @@ -2460,17 +2460,14 @@
    35.4  
    35.5  (* outer syntax *)
    35.6  
    35.7 -local structure P = OuterParse and K = OuterKeyword in
    35.8 -
    35.9  val _ =
   35.10 -  OuterSyntax.command "record" "define extensible record" K.thy_decl
   35.11 -    (P.type_args_constrained -- P.binding --
   35.12 -      (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const_binding)
   35.13 +  Outer_Syntax.command "record" "define extensible record" Keyword.thy_decl
   35.14 +    (Parse.type_args_constrained -- Parse.binding --
   35.15 +      (Parse.$$$ "=" |-- Scan.option (Parse.typ --| Parse.$$$ "+") --
   35.16 +        Scan.repeat1 Parse.const_binding)
   35.17      >> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd false x y z)));
   35.18  
   35.19  end;
   35.20  
   35.21 -end;
   35.22 -
   35.23  structure Basic_Record: BASIC_RECORD = Record;
   35.24  open Basic_Record;
    36.1 --- a/src/HOL/Tools/refute_isar.ML	Mon May 17 15:11:25 2010 +0200
    36.2 +++ b/src/HOL/Tools/refute_isar.ML	Mon May 17 23:54:15 2010 +0200
    36.3 @@ -12,19 +12,16 @@
    36.4  
    36.5  (*optional list of arguments of the form [name1=value1, name2=value2, ...]*)
    36.6  
    36.7 -val scan_parm =
    36.8 -  OuterParse.name
    36.9 -  -- (Scan.optional (OuterParse.$$$ "=" |-- OuterParse.name) "true")
   36.10 -val scan_parms = Scan.optional
   36.11 -  (OuterParse.$$$ "[" |-- OuterParse.list scan_parm --| OuterParse.$$$ "]") [];
   36.12 +val scan_parm = Parse.name -- (Scan.optional (Parse.$$$ "=" |-- Parse.name) "true")
   36.13 +val scan_parms = Scan.optional (Parse.$$$ "[" |-- Parse.list scan_parm --| Parse.$$$ "]") [];
   36.14  
   36.15  
   36.16  (* 'refute' command *)
   36.17  
   36.18  val _ =
   36.19 -  OuterSyntax.improper_command "refute"
   36.20 -    "try to find a model that refutes a given subgoal" OuterKeyword.diag
   36.21 -    (scan_parms -- Scan.optional OuterParse.nat 1 >>
   36.22 +  Outer_Syntax.improper_command "refute"
   36.23 +    "try to find a model that refutes a given subgoal" Keyword.diag
   36.24 +    (scan_parms -- Scan.optional Parse.nat 1 >>
   36.25        (fn (parms, i) =>
   36.26          Toplevel.keep (fn state =>
   36.27            let
   36.28 @@ -36,8 +33,8 @@
   36.29  (* 'refute_params' command *)
   36.30  
   36.31  val _ =
   36.32 -  OuterSyntax.command "refute_params"
   36.33 -    "show/store default parameters for the 'refute' command" OuterKeyword.thy_decl
   36.34 +  Outer_Syntax.command "refute_params"
   36.35 +    "show/store default parameters for the 'refute' command" Keyword.thy_decl
   36.36      (scan_parms >> (fn parms =>
   36.37        Toplevel.theory (fn thy =>
   36.38          let
    37.1 --- a/src/HOL/Tools/split_rule.ML	Mon May 17 15:11:25 2010 +0200
    37.2 +++ b/src/HOL/Tools/split_rule.ML	Mon May 17 23:54:15 2010 +0200
    37.3 @@ -135,7 +135,7 @@
    37.4    Attrib.setup @{binding split_format}
    37.5      (Scan.lift
    37.6       (Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule)) ||
    37.7 -      OuterParse.and_list1 (Scan.repeat Args.name_source)
    37.8 +      Parse.and_list1 (Scan.repeat Args.name_source)
    37.9          >> (fn xss => Thm.rule_attribute (fn context =>
   37.10              split_rule_goal (Context.proof_of context) xss))))
   37.11      "split pair-typed subterms in premises, or function arguments" #>
    38.1 --- a/src/HOL/Tools/typedef.ML	Mon May 17 15:11:25 2010 +0200
    38.2 +++ b/src/HOL/Tools/typedef.ML	Mon May 17 23:54:15 2010 +0200
    38.3 @@ -296,22 +296,19 @@
    38.4  
    38.5  (** outer syntax **)
    38.6  
    38.7 -local structure P = OuterParse in
    38.8 -
    38.9 -val _ = OuterKeyword.keyword "morphisms";
   38.10 +val _ = Keyword.keyword "morphisms";
   38.11  
   38.12  val _ =
   38.13 -  OuterSyntax.local_theory_to_proof "typedef" "HOL type definition (requires non-emptiness proof)"
   38.14 -    OuterKeyword.thy_goal
   38.15 -    (Scan.optional (P.$$$ "(" |--
   38.16 -        ((P.$$$ "open" >> K false) -- Scan.option P.binding ||
   38.17 -          P.binding >> (fn s => (true, SOME s))) --| P.$$$ ")") (true, NONE) --
   38.18 -      (P.type_args_constrained -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) --
   38.19 -      Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding))
   38.20 +  Outer_Syntax.local_theory_to_proof "typedef" "HOL type definition (requires non-emptiness proof)"
   38.21 +    Keyword.thy_goal
   38.22 +    (Scan.optional (Parse.$$$ "(" |--
   38.23 +        ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
   38.24 +          Parse.binding >> (fn s => (true, SOME s))) --| Parse.$$$ ")") (true, NONE) --
   38.25 +      (Parse.type_args_constrained -- Parse.binding) --
   38.26 +        Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.term) --
   38.27 +        Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding))
   38.28      >> (fn ((((((def, opt_name), (args, t)), mx), A), morphs)) =>
   38.29          typedef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs)));
   38.30  
   38.31  end;
   38.32  
   38.33 -end;
   38.34 -
    39.1 --- a/src/HOLCF/IOA/meta_theory/automaton.ML	Mon May 17 15:11:25 2010 +0200
    39.2 +++ b/src/HOLCF/IOA/meta_theory/automaton.ML	Mon May 17 23:54:15 2010 +0200
    39.3 @@ -485,52 +485,50 @@
    39.4  
    39.5  (* outer syntax *)
    39.6  
    39.7 -local structure P = OuterParse and K = OuterKeyword in
    39.8 -
    39.9 -val _ = List.app OuterKeyword.keyword ["signature", "actions", "inputs",
   39.10 +val _ = List.app Keyword.keyword ["signature", "actions", "inputs",
   39.11    "outputs", "internals", "states", "initially", "transitions", "pre",
   39.12    "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
   39.13    "rename"];
   39.14  
   39.15 -val actionlist = P.list1 P.term;
   39.16 -val inputslist = P.$$$ "inputs" |-- P.!!! actionlist;
   39.17 -val outputslist = P.$$$ "outputs" |-- P.!!! actionlist;
   39.18 -val internalslist = P.$$$ "internals" |-- P.!!! actionlist;
   39.19 -val stateslist = P.$$$ "states" |-- P.!!! (Scan.repeat1 (P.name --| P.$$$ "::" -- P.typ));
   39.20 -val initial = P.$$$ "initially" |-- P.!!! P.term;
   39.21 -val assign_list = P.list1 (P.name --| P.$$$ ":=" -- P.!!! P.term);
   39.22 -val pre = P.$$$ "pre" |-- P.!!! P.term;
   39.23 -val post = P.$$$ "post" |-- P.!!! assign_list;
   39.24 +val actionlist = Parse.list1 Parse.term;
   39.25 +val inputslist = Parse.$$$ "inputs" |-- Parse.!!! actionlist;
   39.26 +val outputslist = Parse.$$$ "outputs" |-- Parse.!!! actionlist;
   39.27 +val internalslist = Parse.$$$ "internals" |-- Parse.!!! actionlist;
   39.28 +val stateslist =
   39.29 +  Parse.$$$ "states" |-- Parse.!!! (Scan.repeat1 (Parse.name --| Parse.$$$ "::" -- Parse.typ));
   39.30 +val initial = Parse.$$$ "initially" |-- Parse.!!! Parse.term;
   39.31 +val assign_list = Parse.list1 (Parse.name --| Parse.$$$ ":=" -- Parse.!!! Parse.term);
   39.32 +val pre = Parse.$$$ "pre" |-- Parse.!!! Parse.term;
   39.33 +val post = Parse.$$$ "post" |-- Parse.!!! assign_list;
   39.34  val pre1 = (pre -- (Scan.optional post [])) >> mk_trans_of_prepost;
   39.35  val post1 = ((Scan.optional pre "True") -- post) >> mk_trans_of_prepost;
   39.36 -val transrel =  (P.$$$ "transrel" |-- P.!!! P.term) >> mk_trans_of_rel;
   39.37 -val transition = P.term -- (transrel || pre1 || post1);
   39.38 -val translist = P.$$$ "transitions" |-- P.!!! (Scan.repeat1 transition);
   39.39 +val transrel =  (Parse.$$$ "transrel" |-- Parse.!!! Parse.term) >> mk_trans_of_rel;
   39.40 +val transition = Parse.term -- (transrel || pre1 || post1);
   39.41 +val translist = Parse.$$$ "transitions" |-- Parse.!!! (Scan.repeat1 transition);
   39.42  
   39.43  val ioa_decl =
   39.44 -  (P.name -- (P.$$$ "=" |--
   39.45 -    (P.$$$ "signature" |--
   39.46 -      P.!!! (P.$$$ "actions" |--
   39.47 -        (P.typ --
   39.48 +  (Parse.name -- (Parse.$$$ "=" |--
   39.49 +    (Parse.$$$ "signature" |--
   39.50 +      Parse.!!! (Parse.$$$ "actions" |--
   39.51 +        (Parse.typ --
   39.52            (Scan.optional inputslist []) --
   39.53            (Scan.optional outputslist []) --
   39.54            (Scan.optional internalslist []) --
   39.55            stateslist --
   39.56            (Scan.optional initial "True") --
   39.57          translist))))) >> mk_ioa_decl ||
   39.58 -  (P.name -- (P.$$$ "=" |-- (P.$$$ "compose" |-- P.!!! (P.list1 P.name))))
   39.59 +  (Parse.name -- (Parse.$$$ "=" |-- (Parse.$$$ "compose" |-- Parse.!!! (Parse.list1 Parse.name))))
   39.60      >> mk_composition_decl ||
   39.61 -  (P.name -- (P.$$$ "=" |-- (P.$$$ "hide_action" |--
   39.62 -      P.!!! (P.list1 P.term -- (P.$$$ "in" |-- P.name))))) >> mk_hiding_decl ||
   39.63 -  (P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |--
   39.64 -      P.!!! (P.name -- (P.$$$ "to" |-- P.list1 P.term))))) >> mk_restriction_decl ||
   39.65 -  (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- (P.!!! (P.name -- (P.$$$ "to" |-- P.term))))))
   39.66 +  (Parse.name -- (Parse.$$$ "=" |-- (Parse.$$$ "hide_action" |--
   39.67 +      Parse.!!! (Parse.list1 Parse.term -- (Parse.$$$ "in" |-- Parse.name))))) >> mk_hiding_decl ||
   39.68 +  (Parse.name -- (Parse.$$$ "=" |-- (Parse.$$$ "restrict" |--
   39.69 +      Parse.!!! (Parse.name -- (Parse.$$$ "to" |-- Parse.list1 Parse.term))))) >> mk_restriction_decl ||
   39.70 +  (Parse.name -- (Parse.$$$ "=" |--
   39.71 +      (Parse.$$$ "rename" |-- (Parse.!!! (Parse.name -- (Parse.$$$ "to" |-- Parse.term))))))
   39.72      >> mk_rename_decl;
   39.73  
   39.74  val _ =
   39.75 -  OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" K.thy_decl
   39.76 +  Outer_Syntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" Keyword.thy_decl
   39.77      (ioa_decl >> Toplevel.theory);
   39.78  
   39.79  end;
   39.80 -
   39.81 -end;
    40.1 --- a/src/HOLCF/Tools/Domain/domain_extender.ML	Mon May 17 15:11:25 2010 +0200
    40.2 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Mon May 17 23:54:15 2010 +0200
    40.3 @@ -224,27 +224,25 @@
    40.4  
    40.5  (** outer syntax **)
    40.6  
    40.7 -local structure P = OuterParse and K = OuterKeyword in
    40.8 -
    40.9 -val _ = OuterKeyword.keyword "lazy";
   40.10 +val _ = Keyword.keyword "lazy";
   40.11  
   40.12  val dest_decl : (bool * binding option * string) parser =
   40.13 -  P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
   40.14 -    (P.binding >> SOME) -- (P.$$$ "::" |-- P.typ)  --| P.$$$ ")" >> P.triple1
   40.15 -    || P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")"
   40.16 +  Parse.$$$ "(" |-- Scan.optional (Parse.$$$ "lazy" >> K true) false --
   40.17 +    (Parse.binding >> SOME) -- (Parse.$$$ "::" |-- Parse.typ)  --| Parse.$$$ ")" >> Parse.triple1
   40.18 +    || Parse.$$$ "(" |-- Parse.$$$ "lazy" |-- Parse.typ --| Parse.$$$ ")"
   40.19      >> (fn t => (true,NONE,t))
   40.20 -    || P.typ >> (fn t => (false,NONE,t));
   40.21 +    || Parse.typ >> (fn t => (false,NONE,t));
   40.22  
   40.23  val cons_decl =
   40.24 -  P.binding -- Scan.repeat dest_decl -- P.opt_mixfix;
   40.25 +  Parse.binding -- Scan.repeat dest_decl -- Parse.opt_mixfix;
   40.26  
   40.27  val domain_decl =
   40.28 -  (P.type_args_constrained -- P.binding -- P.opt_mixfix) --
   40.29 -    (P.$$$ "=" |-- P.enum1 "|" cons_decl);
   40.30 +  (Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix) --
   40.31 +    (Parse.$$$ "=" |-- Parse.enum1 "|" cons_decl);
   40.32  
   40.33  val domains_decl =
   40.34 -  Scan.option (P.$$$ "(" |-- P.binding --| P.$$$ ")") --
   40.35 -    P.and_list1 domain_decl;
   40.36 +  Scan.option (Parse.$$$ "(" |-- Parse.binding --| Parse.$$$ ")") --
   40.37 +    Parse.and_list1 domain_decl;
   40.38  
   40.39  fun mk_domain
   40.40      (definitional : bool)
   40.41 @@ -267,13 +265,11 @@
   40.42    end;
   40.43  
   40.44  val _ =
   40.45 -  OuterSyntax.command "domain" "define recursive domains (HOLCF)"
   40.46 -    K.thy_decl (domains_decl >> (Toplevel.theory o mk_domain false));
   40.47 +  Outer_Syntax.command "domain" "define recursive domains (HOLCF)"
   40.48 +    Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain false));
   40.49  
   40.50  val _ =
   40.51 -  OuterSyntax.command "new_domain" "define recursive domains (HOLCF)"
   40.52 -    K.thy_decl (domains_decl >> (Toplevel.theory o mk_domain true));
   40.53 +  Outer_Syntax.command "new_domain" "define recursive domains (HOLCF)"
   40.54 +    Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain true));
   40.55  
   40.56  end;
   40.57 -
   40.58 -end;
    41.1 --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon May 17 15:11:25 2010 +0200
    41.2 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon May 17 23:54:15 2010 +0200
    41.3 @@ -707,21 +707,20 @@
    41.4  
    41.5  local
    41.6  
    41.7 -structure P = OuterParse and K = OuterKeyword
    41.8 -
    41.9  val parse_domain_iso :
   41.10      (string list * binding * mixfix * string * (binding * binding) option)
   41.11        parser =
   41.12 -  (P.type_args -- P.binding -- P.opt_mixfix -- (P.$$$ "=" |-- P.typ) --
   41.13 -    Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding)))
   41.14 +  (Parse.type_args -- Parse.binding -- Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) --
   41.15 +    Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding)))
   41.16      >> (fn ((((vs, t), mx), rhs), morphs) => (vs, t, mx, rhs, morphs));
   41.17  
   41.18 -val parse_domain_isos = P.and_list1 parse_domain_iso;
   41.19 +val parse_domain_isos = Parse.and_list1 parse_domain_iso;
   41.20  
   41.21  in
   41.22  
   41.23  val _ =
   41.24 -  OuterSyntax.command "domain_isomorphism" "define domain isomorphisms (HOLCF)" K.thy_decl
   41.25 +  Outer_Syntax.command "domain_isomorphism" "define domain isomorphisms (HOLCF)"
   41.26 +    Keyword.thy_decl
   41.27      (parse_domain_isos >> (Toplevel.theory o domain_isomorphism_cmd));
   41.28  
   41.29  end;
    42.1 --- a/src/HOLCF/Tools/cont_consts.ML	Mon May 17 15:11:25 2010 +0200
    42.2 +++ b/src/HOLCF/Tools/cont_consts.ML	Mon May 17 23:54:15 2010 +0200
    42.3 @@ -93,12 +93,8 @@
    42.4  
    42.5  (* outer syntax *)
    42.6  
    42.7 -local structure P = OuterParse and K = OuterKeyword in
    42.8 -
    42.9  val _ =
   42.10 -  OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl
   42.11 -    (Scan.repeat1 P.const_binding >> (Toplevel.theory o add_consts_cmd));
   42.12 +  Outer_Syntax.command "consts" "declare constants (HOLCF)" Keyword.thy_decl
   42.13 +    (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o add_consts_cmd));
   42.14  
   42.15  end;
   42.16 -
   42.17 -end;
    43.1 --- a/src/HOLCF/Tools/fixrec.ML	Mon May 17 15:11:25 2010 +0200
    43.2 +++ b/src/HOLCF/Tools/fixrec.ML	Mon May 17 23:54:15 2010 +0200
    43.3 @@ -443,16 +443,14 @@
    43.4  (******************************** Parsers ********************************)
    43.5  (*************************************************************************)
    43.6  
    43.7 -local structure P = OuterParse and K = OuterKeyword in
    43.8 +val _ =
    43.9 +  Outer_Syntax.local_theory "fixrec" "define recursive functions (HOLCF)" Keyword.thy_decl
   43.10 +    ((Parse.opt_keyword "permissive" >> not) -- Parse.fixes -- Parse_Spec.where_alt_specs
   43.11 +      >> (fn ((strict, fixes), specs) => add_fixrec_cmd strict fixes specs));
   43.12  
   43.13 -val _ = OuterSyntax.local_theory "fixrec" "define recursive functions (HOLCF)" K.thy_decl
   43.14 -  ((P.opt_keyword "permissive" >> not) -- P.fixes -- Parse_Spec.where_alt_specs
   43.15 -    >> (fn ((strict, fixes), specs) => add_fixrec_cmd strict fixes specs));
   43.16 -
   43.17 -val _ = OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl
   43.18 -  (Parse_Spec.specs >> (Toplevel.theory o add_fixpat_cmd));
   43.19 -
   43.20 -end;
   43.21 +val _ =
   43.22 +  Outer_Syntax.command "fixpat" "define rewrites for fixrec functions" Keyword.thy_decl
   43.23 +    (Parse_Spec.specs >> (Toplevel.theory o add_fixpat_cmd));
   43.24  
   43.25  val setup =
   43.26    Attrib.setup @{binding fixrec_simp}
    44.1 --- a/src/HOLCF/Tools/pcpodef.ML	Mon May 17 15:11:25 2010 +0200
    44.2 +++ b/src/HOLCF/Tools/pcpodef.ML	Mon May 17 23:54:15 2010 +0200
    44.3 @@ -355,29 +355,29 @@
    44.4  
    44.5  (** outer syntax **)
    44.6  
    44.7 -local structure P = OuterParse and K = OuterKeyword in
    44.8 -
    44.9  val typedef_proof_decl =
   44.10 -  Scan.optional (P.$$$ "(" |--
   44.11 -      ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
   44.12 -        --| P.$$$ ")") (true, NONE) --
   44.13 -    (P.type_args_constrained -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) --
   44.14 -    Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
   44.15 +  Scan.optional (Parse.$$$ "(" |--
   44.16 +      ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
   44.17 +        Parse.binding >> (fn s => (true, SOME s)))
   44.18 +        --| Parse.$$$ ")") (true, NONE) --
   44.19 +    (Parse.type_args_constrained -- Parse.binding) -- Parse.opt_mixfix --
   44.20 +    (Parse.$$$ "=" |-- Parse.term) --
   44.21 +    Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding));
   44.22  
   44.23  fun mk_pcpodef_proof pcpo ((((((def, opt_name), (args, t)), mx), A), morphs)) =
   44.24    (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
   44.25      ((def, the_default t opt_name), (t, args, mx), A, morphs);
   44.26  
   44.27  val _ =
   44.28 -  OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
   44.29 +  Outer_Syntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)"
   44.30 +  Keyword.thy_goal
   44.31      (typedef_proof_decl >>
   44.32        (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)));
   44.33  
   44.34  val _ =
   44.35 -  OuterSyntax.command "cpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
   44.36 +  Outer_Syntax.command "cpodef" "HOLCF type definition (requires admissibility proof)"
   44.37 +  Keyword.thy_goal
   44.38      (typedef_proof_decl >>
   44.39        (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)));
   44.40  
   44.41  end;
   44.42 -
   44.43 -end;
    45.1 --- a/src/HOLCF/Tools/repdef.ML	Mon May 17 15:11:25 2010 +0200
    45.2 +++ b/src/HOLCF/Tools/repdef.ML	Mon May 17 23:54:15 2010 +0200
    45.3 @@ -168,23 +168,21 @@
    45.4  
    45.5  (** outer syntax **)
    45.6  
    45.7 -local structure P = OuterParse and K = OuterKeyword in
    45.8 -
    45.9  val repdef_decl =
   45.10 -  Scan.optional (P.$$$ "(" |--
   45.11 -      ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
   45.12 -        --| P.$$$ ")") (true, NONE) --
   45.13 -    (P.type_args_constrained -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) --
   45.14 -    Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
   45.15 +  Scan.optional (Parse.$$$ "(" |--
   45.16 +      ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
   45.17 +        Parse.binding >> (fn s => (true, SOME s)))
   45.18 +        --| Parse.$$$ ")") (true, NONE) --
   45.19 +    (Parse.type_args_constrained -- Parse.binding) --
   45.20 +    Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.term) --
   45.21 +    Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding));
   45.22  
   45.23  fun mk_repdef ((((((def, opt_name), (args, t)), mx), A), morphs)) =
   45.24    repdef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs);
   45.25  
   45.26  val _ =
   45.27 -  OuterSyntax.command "repdef" "HOLCF definition of representable domains" K.thy_decl
   45.28 +  Outer_Syntax.command "repdef" "HOLCF definition of representable domains" Keyword.thy_decl
   45.29      (repdef_decl >>
   45.30        (Toplevel.print oo (Toplevel.theory o mk_repdef)));
   45.31  
   45.32  end;
   45.33 -
   45.34 -end;
    46.1 --- a/src/Provers/blast.ML	Mon May 17 15:11:25 2010 +0200
    46.2 +++ b/src/Provers/blast.ML	Mon May 17 23:54:15 2010 +0200
    46.3 @@ -1309,7 +1309,7 @@
    46.4  val setup =
    46.5    setup_depth_limit #>
    46.6    Method.setup @{binding blast}
    46.7 -    (Scan.lift (Scan.option OuterParse.nat) --| Method.sections Data.cla_modifiers >>
    46.8 +    (Scan.lift (Scan.option Parse.nat) --| Method.sections Data.cla_modifiers >>
    46.9        (fn NONE => Data.cla_meth' blast_tac
   46.10          | SOME lim => Data.cla_meth' (fn cs => depth_tac cs lim)))
   46.11      "classical tableau prover";
    47.1 --- a/src/Provers/clasimp.ML	Mon May 17 15:11:25 2010 +0200
    47.2 +++ b/src/Provers/clasimp.ML	Mon May 17 23:54:15 2010 +0200
    47.3 @@ -275,7 +275,7 @@
    47.4    Method.sections clasimp_modifiers >> K (clasimp_meth' tac);
    47.5  
    47.6  val auto_method =
    47.7 -  Scan.lift (Scan.option (OuterParse.nat -- OuterParse.nat)) --|
    47.8 +  Scan.lift (Scan.option (Parse.nat -- Parse.nat)) --|
    47.9      Method.sections clasimp_modifiers >>
   47.10    (fn NONE => clasimp_meth (CHANGED_PROP o auto_tac)
   47.11      | SOME (m, n) => clasimp_meth (CHANGED_PROP o (fn css => mk_auto_tac css m n)));
    48.1 --- a/src/Provers/classical.ML	Mon May 17 15:11:25 2010 +0200
    48.2 +++ b/src/Provers/classical.ML	Mon May 17 23:54:15 2010 +0200
    48.3 @@ -1015,8 +1015,8 @@
    48.4  (** outer syntax **)
    48.5  
    48.6  val _ =
    48.7 -  OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner"
    48.8 -    OuterKeyword.diag
    48.9 +  Outer_Syntax.improper_command "print_claset" "print context of Classical Reasoner"
   48.10 +    Keyword.diag
   48.11      (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
   48.12        Toplevel.keep (print_cs o claset_of o Toplevel.context_of)));
   48.13  
    49.1 --- a/src/Tools/Code/code_eval.ML	Mon May 17 15:11:25 2010 +0200
    49.2 +++ b/src/Tools/Code/code_eval.ML	Mon May 17 23:54:15 2010 +0200
    49.3 @@ -204,26 +204,24 @@
    49.4  
    49.5  local
    49.6  
    49.7 -structure P = OuterParse
    49.8 -and K = OuterKeyword
    49.9 -
   49.10  val datatypesK = "datatypes";
   49.11  val functionsK = "functions";
   49.12  val fileK = "file";
   49.13  val andK = "and"
   49.14  
   49.15 -val _ = List.app K.keyword [datatypesK, functionsK];
   49.16 +val _ = List.app Keyword.keyword [datatypesK, functionsK];
   49.17  
   49.18 -val parse_datatype = (P.name --| P.$$$ "=" -- (P.term ::: (Scan.repeat (P.$$$ "|" |-- P.term))));
   49.19 +val parse_datatype =
   49.20 +  Parse.name --| Parse.$$$ "=" -- (Parse.term ::: (Scan.repeat (Parse.$$$ "|" |-- Parse.term)));
   49.21  
   49.22  in
   49.23  
   49.24  val _ =
   49.25 -  OuterSyntax.command "code_reflect" "enrich runtime environment with generated code"
   49.26 -    K.thy_decl (P.name -- Scan.optional (P.$$$ datatypesK |-- (parse_datatype
   49.27 -      ::: Scan.repeat (P.$$$ andK |-- parse_datatype))) []
   49.28 -    -- Scan.optional (P.$$$ functionsK |-- Scan.repeat1 P.name) []
   49.29 -    -- Scan.option (P.$$$ fileK |-- P.name)
   49.30 +  Outer_Syntax.command "code_reflect" "enrich runtime environment with generated code"
   49.31 +    Keyword.thy_decl (Parse.name -- Scan.optional (Parse.$$$ datatypesK |-- (parse_datatype
   49.32 +      ::: Scan.repeat (Parse.$$$ andK |-- parse_datatype))) []
   49.33 +    -- Scan.optional (Parse.$$$ functionsK |-- Scan.repeat1 Parse.name) []
   49.34 +    -- Scan.option (Parse.$$$ fileK |-- Parse.name)
   49.35    >> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory
   49.36      (code_reflect_cmd raw_datatypes raw_functions module_name some_file)));
   49.37  
    50.1 --- a/src/Tools/Code/code_haskell.ML	Mon May 17 15:11:25 2010 +0200
    50.2 +++ b/src/Tools/Code/code_haskell.ML	Mon May 17 23:54:15 2010 +0200
    50.3 @@ -469,8 +469,8 @@
    50.4        serialize_haskell module_prefix module_name string_classes));
    50.5  
    50.6  val _ =
    50.7 -  OuterSyntax.command "code_monad" "define code syntax for monads" OuterKeyword.thy_decl (
    50.8 -    OuterParse.term_group -- OuterParse.name >> (fn (raw_bind, target) =>
    50.9 +  Outer_Syntax.command "code_monad" "define code syntax for monads" Keyword.thy_decl (
   50.10 +    Parse.term_group -- Parse.name >> (fn (raw_bind, target) =>
   50.11        Toplevel.theory  (add_monad target raw_bind))
   50.12    );
   50.13  
    51.1 --- a/src/Tools/Code/code_preproc.ML	Mon May 17 15:11:25 2010 +0200
    51.2 +++ b/src/Tools/Code/code_preproc.ML	Mon May 17 23:54:15 2010 +0200
    51.3 @@ -479,8 +479,8 @@
    51.4    end;
    51.5  
    51.6  val _ =
    51.7 -  OuterSyntax.improper_command "print_codeproc" "print code preprocessor setup"
    51.8 -  OuterKeyword.diag (Scan.succeed
    51.9 +  Outer_Syntax.improper_command "print_codeproc" "print code preprocessor setup"
   51.10 +  Keyword.diag (Scan.succeed
   51.11        (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
   51.12          (print_codeproc o Toplevel.theory_of)));
   51.13  
    52.1 --- a/src/Tools/Code/code_printer.ML	Mon May 17 15:11:25 2010 +0200
    52.2 +++ b/src/Tools/Code/code_printer.ML	Mon May 17 23:54:15 2010 +0200
    52.3 @@ -329,15 +329,15 @@
    52.4  
    52.5  fun parse_syntax prep_arg xs =
    52.6    Scan.option ((
    52.7 -      ((OuterParse.$$$ infixK >> K X)
    52.8 -        || (OuterParse.$$$ infixlK >> K L)
    52.9 -        || (OuterParse.$$$ infixrK >> K R))
   52.10 -        -- OuterParse.nat >> parse_infix prep_arg
   52.11 +      ((Parse.$$$ infixK >> K X)
   52.12 +        || (Parse.$$$ infixlK >> K L)
   52.13 +        || (Parse.$$$ infixrK >> K R))
   52.14 +        -- Parse.nat >> parse_infix prep_arg
   52.15        || Scan.succeed (parse_mixfix prep_arg))
   52.16 -      -- OuterParse.string
   52.17 +      -- Parse.string
   52.18        >> (fn (parse, s) => parse s)) xs;
   52.19  
   52.20 -val _ = List.app OuterKeyword.keyword [infixK, infixlK, infixrK];
   52.21 +val _ = List.app Keyword.keyword [infixK, infixlK, infixrK];
   52.22  
   52.23  
   52.24  (** module name spaces **)
    53.1 --- a/src/Tools/Code/code_target.ML	Mon May 17 15:11:25 2010 +0200
    53.2 +++ b/src/Tools/Code/code_target.ML	Mon May 17 23:54:15 2010 +0200
    53.3 @@ -463,9 +463,6 @@
    53.4  
    53.5  local
    53.6  
    53.7 -structure P = OuterParse
    53.8 -and K = OuterKeyword
    53.9 -
   53.10  fun zip_list (x::xs) f g =
   53.11    f
   53.12    #-> (fn y =>
   53.13 @@ -473,9 +470,9 @@
   53.14      #-> (fn xys => pair ((x, y) :: xys)));
   53.15  
   53.16  fun parse_multi_syntax parse_thing parse_syntax =
   53.17 -  P.and_list1 parse_thing
   53.18 -  #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name --
   53.19 -        (zip_list things parse_syntax (P.$$$ "and")) --| P.$$$ ")"));
   53.20 +  Parse.and_list1 parse_thing
   53.21 +  #-> (fn things => Scan.repeat1 (Parse.$$$ "(" |-- Parse.name --
   53.22 +        (zip_list things parse_syntax (Parse.$$$ "and")) --| Parse.$$$ ")"));
   53.23  
   53.24  in
   53.25  
   53.26 @@ -507,75 +504,79 @@
   53.27  val (inK, module_nameK, fileK) = ("in", "module_name", "file");
   53.28  
   53.29  val code_exprP =
   53.30 -  (Scan.repeat1 P.term_group
   53.31 -  -- Scan.repeat (P.$$$ inK |-- P.name
   53.32 -     -- Scan.option (P.$$$ module_nameK |-- P.name)
   53.33 -     -- Scan.option (P.$$$ fileK |-- P.name)
   53.34 -     -- Scan.optional (P.$$$ "(" |-- Args.parse --| P.$$$ ")") []
   53.35 +  (Scan.repeat1 Parse.term_group
   53.36 +  -- Scan.repeat (Parse.$$$ inK |-- Parse.name
   53.37 +     -- Scan.option (Parse.$$$ module_nameK |-- Parse.name)
   53.38 +     -- Scan.option (Parse.$$$ fileK |-- Parse.name)
   53.39 +     -- Scan.optional (Parse.$$$ "(" |-- Args.parse --| Parse.$$$ ")") []
   53.40    ) >> (fn (raw_cs, seris) => export_code_cmd raw_cs seris));
   53.41  
   53.42 -val _ = List.app OuterKeyword.keyword [inK, module_nameK, fileK];
   53.43 +val _ = List.app Keyword.keyword [inK, module_nameK, fileK];
   53.44  
   53.45  val _ =
   53.46 -  OuterSyntax.command "code_class" "define code syntax for class" K.thy_decl (
   53.47 -    parse_multi_syntax P.xname (Scan.option P.string)
   53.48 +  Outer_Syntax.command "code_class" "define code syntax for class" Keyword.thy_decl (
   53.49 +    parse_multi_syntax Parse.xname (Scan.option Parse.string)
   53.50      >> (Toplevel.theory oo fold) (fn (target, syns) =>
   53.51            fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)
   53.52    );
   53.53  
   53.54  val _ =
   53.55 -  OuterSyntax.command "code_instance" "define code syntax for instance" K.thy_decl (
   53.56 -    parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname) (Scan.option (P.minus >> K ()))
   53.57 +  Outer_Syntax.command "code_instance" "define code syntax for instance" Keyword.thy_decl (
   53.58 +    parse_multi_syntax (Parse.xname --| Parse.$$$ "::" -- Parse.xname)
   53.59 +      (Scan.option (Parse.minus >> K ()))
   53.60      >> (Toplevel.theory oo fold) (fn (target, syns) =>
   53.61            fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns)
   53.62    );
   53.63  
   53.64  val _ =
   53.65 -  OuterSyntax.command "code_type" "define code syntax for type constructor" K.thy_decl (
   53.66 -    parse_multi_syntax P.xname (Code_Printer.parse_syntax I)
   53.67 +  Outer_Syntax.command "code_type" "define code syntax for type constructor" Keyword.thy_decl (
   53.68 +    parse_multi_syntax Parse.xname (Code_Printer.parse_syntax I)
   53.69      >> (Toplevel.theory oo fold) (fn (target, syns) =>
   53.70            fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns)
   53.71    );
   53.72  
   53.73  val _ =
   53.74 -  OuterSyntax.command "code_const" "define code syntax for constant" K.thy_decl (
   53.75 -    parse_multi_syntax P.term_group (Code_Printer.parse_syntax fst)
   53.76 +  Outer_Syntax.command "code_const" "define code syntax for constant" Keyword.thy_decl (
   53.77 +    parse_multi_syntax Parse.term_group (Code_Printer.parse_syntax fst)
   53.78      >> (Toplevel.theory oo fold) (fn (target, syns) =>
   53.79        fold (fn (raw_const, syn) => add_syntax_const_simple_cmd target raw_const syn) syns)
   53.80    );
   53.81  
   53.82  val _ =
   53.83 -  OuterSyntax.command "code_reserved" "declare words as reserved for target language" K.thy_decl (
   53.84 -    P.name -- Scan.repeat1 P.name
   53.85 +  Outer_Syntax.command "code_reserved" "declare words as reserved for target language"
   53.86 +    Keyword.thy_decl (
   53.87 +    Parse.name -- Scan.repeat1 Parse.name
   53.88      >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds)
   53.89    );
   53.90  
   53.91  val _ =
   53.92 -  OuterSyntax.command "code_include" "declare piece of code to be included in generated code" K.thy_decl (
   53.93 -    P.name -- P.name -- (P.text :|-- (fn "-" => Scan.succeed NONE
   53.94 -      | s => Scan.optional (P.$$$ "attach" |-- Scan.repeat1 P.term) [] >> pair s >> SOME))
   53.95 +  Outer_Syntax.command "code_include" "declare piece of code to be included in generated code"
   53.96 +    Keyword.thy_decl (
   53.97 +    Parse.name -- Parse.name -- (Parse.text :|-- (fn "-" => Scan.succeed NONE
   53.98 +      | s => Scan.optional (Parse.$$$ "attach" |-- Scan.repeat1 Parse.term) [] >> pair s >> SOME))
   53.99      >> (fn ((target, name), content_consts) =>
  53.100          (Toplevel.theory o add_include_cmd target) (name, content_consts))
  53.101    );
  53.102  
  53.103  val _ =
  53.104 -  OuterSyntax.command "code_modulename" "alias module to other name" K.thy_decl (
  53.105 -    P.name -- Scan.repeat1 (P.name -- P.name)
  53.106 +  Outer_Syntax.command "code_modulename" "alias module to other name" Keyword.thy_decl (
  53.107 +    Parse.name -- Scan.repeat1 (Parse.name -- Parse.name)
  53.108      >> (fn (target, modlnames) => (Toplevel.theory o fold (add_module_alias target)) modlnames)
  53.109    );
  53.110  
  53.111  val _ =
  53.112 -  OuterSyntax.command "code_abort" "permit constant to be implemented as program abort" K.thy_decl (
  53.113 -    Scan.repeat1 P.term_group >> (Toplevel.theory o fold allow_abort_cmd)
  53.114 +  Outer_Syntax.command "code_abort" "permit constant to be implemented as program abort"
  53.115 +    Keyword.thy_decl (
  53.116 +    Scan.repeat1 Parse.term_group >> (Toplevel.theory o fold allow_abort_cmd)
  53.117    );
  53.118  
  53.119  val _ =
  53.120 -  OuterSyntax.command "export_code" "generate executable code for constants"
  53.121 -    K.diag (P.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
  53.122 +  Outer_Syntax.command "export_code" "generate executable code for constants"
  53.123 +    Keyword.diag (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
  53.124  
  53.125  fun shell_command thyname cmd = Toplevel.program (fn _ =>
  53.126 -  (use_thy thyname; case Scan.read Token.stopper (P.!!! code_exprP)
  53.127 -    ((filter Token.is_proper o OuterSyntax.scan Position.none) cmd)
  53.128 +  (use_thy thyname; case Scan.read Token.stopper (Parse.!!! code_exprP)
  53.129 +    ((filter Token.is_proper o Outer_Syntax.scan Position.none) cmd)
  53.130     of SOME f => (writeln "Now generating code..."; f (theory thyname))
  53.131      | NONE => error ("Bad directive " ^ quote cmd)))
  53.132    handle Runtime.TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
    54.1 --- a/src/Tools/Code/code_thingol.ML	Mon May 17 15:11:25 2010 +0200
    54.2 +++ b/src/Tools/Code/code_thingol.ML	Mon May 17 23:54:15 2010 +0200
    54.3 @@ -915,23 +915,21 @@
    54.4  
    54.5  local
    54.6  
    54.7 -structure P = OuterParse
    54.8 -and K = OuterKeyword
    54.9 -
   54.10  fun code_thms_cmd thy = code_thms thy o op @ o read_const_exprs thy;
   54.11  fun code_deps_cmd thy = code_deps thy o op @ o read_const_exprs thy;
   54.12  
   54.13  in
   54.14  
   54.15  val _ =
   54.16 -  OuterSyntax.improper_command "code_thms" "print system of code equations for code" OuterKeyword.diag
   54.17 -    (Scan.repeat1 P.term_group
   54.18 +  Outer_Syntax.improper_command "code_thms" "print system of code equations for code" Keyword.diag
   54.19 +    (Scan.repeat1 Parse.term_group
   54.20        >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
   54.21          o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
   54.22  
   54.23  val _ =
   54.24 -  OuterSyntax.improper_command "code_deps" "visualize dependencies of code equations for code" OuterKeyword.diag
   54.25 -    (Scan.repeat1 P.term_group
   54.26 +  Outer_Syntax.improper_command "code_deps" "visualize dependencies of code equations for code"
   54.27 +    Keyword.diag
   54.28 +    (Scan.repeat1 Parse.term_group
   54.29        >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
   54.30          o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
   54.31  
    55.1 --- a/src/Tools/WWW_Find/find_theorems.ML	Mon May 17 15:11:25 2010 +0200
    55.2 +++ b/src/Tools/WWW_Find/find_theorems.ML	Mon May 17 23:54:15 2010 +0200
    55.3 @@ -158,21 +158,17 @@
    55.4  
    55.5  end;
    55.6  
    55.7 -structure P = OuterParse
    55.8 -      and K = OuterKeyword
    55.9 -      and FT = Find_Theorems;
   55.10 -
   55.11  val criterion =
   55.12 -  P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Find_Theorems.Name ||
   55.13 -  P.reserved "intro" >> K Find_Theorems.Intro ||
   55.14 -  P.reserved "elim" >> K Find_Theorems.Elim ||
   55.15 -  P.reserved "dest" >> K Find_Theorems.Dest ||
   55.16 -  P.reserved "solves" >> K Find_Theorems.Solves ||
   55.17 -  P.reserved "simp" |-- P.!!! (P.$$$ ":" |-- P.term) >> Find_Theorems.Simp ||
   55.18 -  P.term >> Find_Theorems.Pattern;
   55.19 +  Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Find_Theorems.Name ||
   55.20 +  Parse.reserved "intro" >> K Find_Theorems.Intro ||
   55.21 +  Parse.reserved "elim" >> K Find_Theorems.Elim ||
   55.22 +  Parse.reserved "dest" >> K Find_Theorems.Dest ||
   55.23 +  Parse.reserved "solves" >> K Find_Theorems.Solves ||
   55.24 +  Parse.reserved "simp" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.term) >> Find_Theorems.Simp ||
   55.25 +  Parse.term >> Find_Theorems.Pattern;
   55.26  
   55.27  val parse_query =
   55.28 -  Scan.repeat (((Scan.option P.minus >> is_none) -- criterion));
   55.29 +  Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion));
   55.30  
   55.31  fun app_index f xs = fold_index (fn x => K (f x)) xs ();
   55.32  
   55.33 @@ -194,7 +190,7 @@
   55.34      fun get_query () =
   55.35        query
   55.36        |> (fn s => s ^ ";")
   55.37 -      |> OuterSyntax.scan Position.start
   55.38 +      |> Outer_Syntax.scan Position.start
   55.39        |> filter Token.is_proper
   55.40        |> Scan.error parse_query
   55.41        |> fst;
    56.1 --- a/src/Tools/WWW_Find/unicode_symbols.ML	Mon May 17 15:11:25 2010 +0200
    56.2 +++ b/src/Tools/WWW_Find/unicode_symbols.ML	Mon May 17 23:54:15 2010 +0200
    56.3 @@ -114,8 +114,6 @@
    56.4  
    56.5  local (* Parser *)
    56.6  
    56.7 -structure P = OuterParse;
    56.8 -
    56.9  fun $$$ kw = Scan.one (is_keyword kw) >> str_of_token;
   56.10  val hex_code = Scan.one is_hex_code >> int_of_code;
   56.11  val ascii_sym = Scan.one is_ascii_sym >> str_of_token;
   56.12 @@ -129,7 +127,7 @@
   56.13  
   56.14  in
   56.15  
   56.16 -val line = (symbol -- unicode --| font -- abbr) >> P.triple1;
   56.17 +val line = (symbol -- unicode --| font -- abbr) >> Parse.triple1;
   56.18  
   56.19  val symbols_path =
   56.20    [getenv "ISABELLE_HOME", "etc", "symbols"]
    57.1 --- a/src/Tools/eqsubst.ML	Mon May 17 15:11:25 2010 +0200
    57.2 +++ b/src/Tools/eqsubst.ML	Mon May 17 23:54:15 2010 +0200
    57.3 @@ -556,7 +556,7 @@
    57.4       (Scan.succeed false);
    57.5  
    57.6  val ith_syntax =
    57.7 -    Scan.optional (Args.parens (Scan.repeat OuterParse.nat)) [0];
    57.8 +    Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0];
    57.9  
   57.10  (* combination method that takes a flag (true indicates that subst
   57.11     should be done to an assumption, false = apply to the conclusion of
    58.1 --- a/src/Tools/induct.ML	Mon May 17 15:11:25 2010 +0200
    58.2 +++ b/src/Tools/induct.ML	Mon May 17 23:54:15 2010 +0200
    58.3 @@ -254,8 +254,8 @@
    58.4    end;
    58.5  
    58.6  val _ =
    58.7 -  OuterSyntax.improper_command "print_induct_rules" "print induction and cases rules"
    58.8 -    OuterKeyword.diag (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
    58.9 +  Outer_Syntax.improper_command "print_induct_rules" "print induction and cases rules"
   58.10 +    Keyword.diag (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
   58.11        Toplevel.keep (print_rules o Toplevel.context_of)));
   58.12  
   58.13  
   58.14 @@ -845,8 +845,6 @@
   58.15  
   58.16  (** concrete syntax **)
   58.17  
   58.18 -structure P = OuterParse;
   58.19 -
   58.20  val arbitraryN = "arbitrary";
   58.21  val takingN = "taking";
   58.22  val ruleN = "rule";
   58.23 @@ -892,7 +890,7 @@
   58.24      Args.$$$ predN || Args.$$$ setN || Args.$$$ ruleN) -- Args.colon)) scan;
   58.25  
   58.26  val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |--
   58.27 -  P.and_list1' (Scan.repeat (unless_more_args free))) [];
   58.28 +  Parse.and_list1' (Scan.repeat (unless_more_args free))) [];
   58.29  
   58.30  val taking = Scan.optional (Scan.lift (Args.$$$ takingN -- Args.colon) |--
   58.31    Scan.repeat1 (unless_more_args inst)) [];
   58.32 @@ -902,7 +900,7 @@
   58.33  val cases_setup =
   58.34    Method.setup @{binding cases}
   58.35      (Args.mode no_simpN --
   58.36 -      (P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
   58.37 +      (Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
   58.38        (fn (no_simp, (insts, opt_rule)) => fn ctxt =>
   58.39          METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL
   58.40            (cases_tac ctxt (not no_simp) insts opt_rule facts)))))
   58.41 @@ -910,11 +908,12 @@
   58.42  
   58.43  val induct_setup =
   58.44    Method.setup @{binding induct}
   58.45 -    (Args.mode no_simpN -- (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
   58.46 +    (Args.mode no_simpN -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
   58.47        (arbitrary -- taking -- Scan.option induct_rule)) >>
   58.48        (fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn ctxt =>
   58.49          RAW_METHOD_CASES (fn facts =>
   58.50 -          Seq.DETERM (HEADGOAL (induct_tac ctxt (not no_simp) insts arbitrary taking opt_rule facts)))))
   58.51 +          Seq.DETERM
   58.52 +            (HEADGOAL (induct_tac ctxt (not no_simp) insts arbitrary taking opt_rule facts)))))
   58.53      "induction on types or predicates/sets";
   58.54  
   58.55  val coinduct_setup =
    59.1 --- a/src/Tools/induct_tacs.ML	Mon May 17 15:11:25 2010 +0200
    59.2 +++ b/src/Tools/induct_tacs.ML	Mon May 17 23:54:15 2010 +0200
    59.3 @@ -116,8 +116,7 @@
    59.4  val opt_rules = Scan.option (rule_spec |-- Attrib.thms);
    59.5  
    59.6  val varss =
    59.7 -  OuterParse.and_list'
    59.8 -    (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_source))));
    59.9 +  Parse.and_list' (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_source))));
   59.10  
   59.11  in
   59.12  
    60.1 --- a/src/Tools/intuitionistic.ML	Mon May 17 15:11:25 2010 +0200
    60.2 +++ b/src/Tools/intuitionistic.ML	Mon May 17 23:54:15 2010 +0200
    60.3 @@ -71,7 +71,7 @@
    60.4  val destN = "dest";
    60.5  
    60.6  fun modifier name kind kind' att =
    60.7 -  Args.$$$ name |-- (kind >> K NONE || kind' |-- OuterParse.nat --| Args.colon >> SOME)
    60.8 +  Args.$$$ name |-- (kind >> K NONE || kind' |-- Parse.nat --| Args.colon >> SOME)
    60.9      >> (pair (I: Proof.context -> Proof.context) o att);
   60.10  
   60.11  val modifiers =
   60.12 @@ -87,7 +87,7 @@
   60.13  
   60.14  fun method_setup name =
   60.15    Method.setup name
   60.16 -    (Scan.lift (Scan.option OuterParse.nat) --| Method.sections modifiers >>
   60.17 +    (Scan.lift (Scan.option Parse.nat) --| Method.sections modifiers >>
   60.18        (fn opt_lim => fn ctxt =>
   60.19          SIMPLE_METHOD' (Object_Logic.atomize_prems_tac THEN' prover_tac ctxt opt_lim)))
   60.20      "intuitionistic proof search";
    61.1 --- a/src/Tools/nbe.ML	Mon May 17 15:11:25 2010 +0200
    61.2 +++ b/src/Tools/nbe.ML	Mon May 17 23:54:15 2010 +0200
    61.3 @@ -625,15 +625,12 @@
    61.4  
    61.5  val setup = Value.add_evaluator ("nbe", norm o ProofContext.theory_of);
    61.6  
    61.7 -local structure P = OuterParse and K = OuterKeyword in
    61.8 -
    61.9 -val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
   61.10 +val opt_modes =
   61.11 +  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
   61.12  
   61.13  val _ =
   61.14 -  OuterSyntax.improper_command "normal_form" "normalize term by evaluation" K.diag
   61.15 -    (opt_modes -- P.term >> (Toplevel.keep o norm_print_term_cmd));
   61.16 -
   61.17 -end;
   61.18 +  Outer_Syntax.improper_command "normal_form" "normalize term by evaluation" Keyword.diag
   61.19 +    (opt_modes -- Parse.term >> (Toplevel.keep o norm_print_term_cmd));
   61.20  
   61.21  end;
   61.22   
   61.23 \ No newline at end of file
    62.1 --- a/src/Tools/quickcheck.ML	Mon May 17 15:11:25 2010 +0200
    62.2 +++ b/src/Tools/quickcheck.ML	Mon May 17 23:54:15 2010 +0200
    62.3 @@ -315,27 +315,25 @@
    62.4      test_goal quiet report generator_name size iterations default_type no_assms insts i assms state
    62.5    end;
    62.6  
    62.7 -fun quickcheck args i state = fst (gen_quickcheck args i state)
    62.8 +fun quickcheck args i state = fst (gen_quickcheck args i state);
    62.9  
   62.10  fun quickcheck_cmd args i state =
   62.11    gen_quickcheck args i (Toplevel.proof_of state)
   62.12    |> Pretty.writeln o pretty_counterex_and_reports (Toplevel.context_of state);
   62.13  
   62.14 -local structure P = OuterParse and K = OuterKeyword in
   62.15 +val parse_arg = Parse.name -- (Scan.optional (Parse.$$$ "=" |-- Parse.name) "true");
   62.16  
   62.17 -val parse_arg = P.name -- (Scan.optional (P.$$$ "=" |-- P.name) "true")
   62.18 -
   62.19 -val parse_args = P.$$$ "[" |-- P.list1 parse_arg --| P.$$$ "]"
   62.20 +val parse_args = Parse.$$$ "[" |-- Parse.list1 parse_arg --| Parse.$$$ "]"
   62.21    || Scan.succeed [];
   62.22  
   62.23 -val _ = OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl
   62.24 -  (parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args)));
   62.25 +val _ =
   62.26 +  Outer_Syntax.command "quickcheck_params" "set parameters for random testing" Keyword.thy_decl
   62.27 +    (parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args)));
   62.28  
   62.29 -val _ = OuterSyntax.improper_command "quickcheck" "try to find counterexample for subgoal" K.diag
   62.30 -  (parse_args -- Scan.optional P.nat 1
   62.31 -    >> (fn (args, i) => Toplevel.no_timing o Toplevel.keep (quickcheck_cmd args i)));
   62.32 -
   62.33 -end; (*local*)
   62.34 +val _ =
   62.35 +  Outer_Syntax.improper_command "quickcheck" "try to find counterexample for subgoal" Keyword.diag
   62.36 +    (parse_args -- Scan.optional Parse.nat 1
   62.37 +      >> (fn (args, i) => Toplevel.no_timing o Toplevel.keep (quickcheck_cmd args i)));
   62.38  
   62.39  end;
   62.40  
    63.1 --- a/src/Tools/value.ML	Mon May 17 15:11:25 2010 +0200
    63.2 +++ b/src/Tools/value.ML	Mon May 17 23:54:15 2010 +0200
    63.3 @@ -52,15 +52,13 @@
    63.4          Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
    63.5    in Pretty.writeln p end;
    63.6  
    63.7 -local structure P = OuterParse and K = OuterKeyword in
    63.8 -
    63.9 -val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
   63.10 +val opt_modes =
   63.11 +  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
   63.12  
   63.13 -val _ = OuterSyntax.improper_command "value" "evaluate and print term" K.diag
   63.14 -  (Scan.option (P.$$$ "[" |-- P.xname --| P.$$$ "]") -- opt_modes -- P.term
   63.15 -    >> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep
   63.16 -        (value_cmd some_name modes t)));
   63.17 -
   63.18 -end; (*local*)
   63.19 +val _ =
   63.20 +  Outer_Syntax.improper_command "value" "evaluate and print term" Keyword.diag
   63.21 +    (Scan.option (Parse.$$$ "[" |-- Parse.xname --| Parse.$$$ "]") -- opt_modes -- Parse.term
   63.22 +      >> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep
   63.23 +          (value_cmd some_name modes t)));
   63.24  
   63.25  end;
    64.1 --- a/src/ZF/Tools/datatype_package.ML	Mon May 17 15:11:25 2010 +0200
    64.2 +++ b/src/ZF/Tools/datatype_package.ML	Mon May 17 23:54:15 2010 +0200
    64.3 @@ -419,29 +419,26 @@
    64.4  
    64.5  (* outer syntax *)
    64.6  
    64.7 -local structure P = OuterParse and K = OuterKeyword in
    64.8 -
    64.9  fun mk_datatype ((((dom, dts), monos), type_intrs), type_elims) =
   64.10    #1 o add_datatype (dom, map fst dts) (map snd dts) (monos, type_intrs, type_elims);
   64.11  
   64.12  val con_decl =
   64.13 -  P.name -- Scan.optional (P.$$$ "(" |-- P.list1 P.term --| P.$$$ ")") [] -- P.opt_mixfix
   64.14 -  >> P.triple1;
   64.15 +  Parse.name -- Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.term --| Parse.$$$ ")") [] --
   64.16 +    Parse.opt_mixfix >> Parse.triple1;
   64.17  
   64.18  val datatype_decl =
   64.19 -  (Scan.optional ((P.$$$ "\<subseteq>" || P.$$$ "<=") |-- P.!!! P.term) "") --
   64.20 -  P.and_list1 (P.term -- (P.$$$ "=" |-- P.enum1 "|" con_decl)) --
   64.21 -  Scan.optional (P.$$$ "monos" |-- P.!!! Parse_Spec.xthms1) [] --
   64.22 -  Scan.optional (P.$$$ "type_intros" |-- P.!!! Parse_Spec.xthms1) [] --
   64.23 -  Scan.optional (P.$$$ "type_elims" |-- P.!!! Parse_Spec.xthms1) []
   64.24 +  (Scan.optional ((Parse.$$$ "\<subseteq>" || Parse.$$$ "<=") |-- Parse.!!! Parse.term) "") --
   64.25 +  Parse.and_list1 (Parse.term -- (Parse.$$$ "=" |-- Parse.enum1 "|" con_decl)) --
   64.26 +  Scan.optional (Parse.$$$ "monos" |-- Parse.!!! Parse_Spec.xthms1) [] --
   64.27 +  Scan.optional (Parse.$$$ "type_intros" |-- Parse.!!! Parse_Spec.xthms1) [] --
   64.28 +  Scan.optional (Parse.$$$ "type_elims" |-- Parse.!!! Parse_Spec.xthms1) []
   64.29    >> (Toplevel.theory o mk_datatype);
   64.30  
   64.31  val coind_prefix = if coind then "co" else "";
   64.32  
   64.33 -val _ = OuterSyntax.command (coind_prefix ^ "datatype")
   64.34 -  ("define " ^ coind_prefix ^ "datatype") K.thy_decl datatype_decl;
   64.35 +val _ =
   64.36 +  Outer_Syntax.command (coind_prefix ^ "datatype")
   64.37 +    ("define " ^ coind_prefix ^ "datatype") Keyword.thy_decl datatype_decl;
   64.38  
   64.39  end;
   64.40  
   64.41 -end;
   64.42 -
    65.1 --- a/src/ZF/Tools/ind_cases.ML	Mon May 17 15:11:25 2010 +0200
    65.2 +++ b/src/ZF/Tools/ind_cases.ML	Mon May 17 23:54:15 2010 +0200
    65.3 @@ -64,15 +64,11 @@
    65.4  
    65.5  (* outer syntax *)
    65.6  
    65.7 -local structure P = OuterParse and K = OuterKeyword in
    65.8 -
    65.9  val _ =
   65.10 -  OuterSyntax.command "inductive_cases"
   65.11 -    "create simplified instances of elimination rules (improper)" K.thy_script
   65.12 -    (P.and_list1 (Parse_Spec.opt_thm_name ":" -- Scan.repeat1 P.prop)
   65.13 +  Outer_Syntax.command "inductive_cases"
   65.14 +    "create simplified instances of elimination rules (improper)" Keyword.thy_script
   65.15 +    (Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Scan.repeat1 Parse.prop)
   65.16        >> (Toplevel.theory o inductive_cases));
   65.17  
   65.18  end;
   65.19  
   65.20 -end;
   65.21 -
    66.1 --- a/src/ZF/Tools/induct_tacs.ML	Mon May 17 15:11:25 2010 +0200
    66.2 +++ b/src/ZF/Tools/induct_tacs.ML	Mon May 17 23:54:15 2010 +0200
    66.3 @@ -186,25 +186,20 @@
    66.4  
    66.5  (* outer syntax *)
    66.6  
    66.7 -local structure P = OuterParse and K = OuterKeyword in
    66.8 -
    66.9 -val _ = List.app OuterKeyword.keyword ["elimination", "induction", "case_eqns", "recursor_eqns"];
   66.10 +val _ = List.app Keyword.keyword ["elimination", "induction", "case_eqns", "recursor_eqns"];
   66.11  
   66.12  val rep_datatype_decl =
   66.13 -  (P.$$$ "elimination" |-- P.!!! Parse_Spec.xthm) --
   66.14 -  (P.$$$ "induction" |-- P.!!! Parse_Spec.xthm) --
   66.15 -  (P.$$$ "case_eqns" |-- P.!!! Parse_Spec.xthms1) --
   66.16 -  Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! Parse_Spec.xthms1) []
   66.17 +  (Parse.$$$ "elimination" |-- Parse.!!! Parse_Spec.xthm) --
   66.18 +  (Parse.$$$ "induction" |-- Parse.!!! Parse_Spec.xthm) --
   66.19 +  (Parse.$$$ "case_eqns" |-- Parse.!!! Parse_Spec.xthms1) --
   66.20 +  Scan.optional (Parse.$$$ "recursor_eqns" |-- Parse.!!! Parse_Spec.xthms1) []
   66.21    >> (fn (((x, y), z), w) => rep_datatype x y z w);
   66.22  
   66.23  val _ =
   66.24 -  OuterSyntax.command "rep_datatype" "represent existing set inductively" K.thy_decl
   66.25 +  Outer_Syntax.command "rep_datatype" "represent existing set inductively" Keyword.thy_decl
   66.26      (rep_datatype_decl >> Toplevel.theory);
   66.27  
   66.28  end;
   66.29  
   66.30 -end;
   66.31 -
   66.32 -
   66.33  val exhaust_tac = DatatypeTactics.exhaust_tac;
   66.34  val induct_tac  = DatatypeTactics.induct_tac;
    67.1 --- a/src/ZF/Tools/inductive_package.ML	Mon May 17 15:11:25 2010 +0200
    67.2 +++ b/src/ZF/Tools/inductive_package.ML	Mon May 17 23:54:15 2010 +0200
    67.3 @@ -576,29 +576,26 @@
    67.4  
    67.5  (* outer syntax *)
    67.6  
    67.7 -local structure P = OuterParse and K = OuterKeyword in
    67.8 -
    67.9 -val _ = List.app OuterKeyword.keyword
   67.10 +val _ = List.app Keyword.keyword
   67.11    ["domains", "intros", "monos", "con_defs", "type_intros", "type_elims"];
   67.12  
   67.13  fun mk_ind (((((doms, intrs), monos), con_defs), type_intrs), type_elims) =
   67.14 -  #1 o add_inductive doms (map P.triple_swap intrs) (monos, con_defs, type_intrs, type_elims);
   67.15 +  #1 o add_inductive doms (map Parse.triple_swap intrs) (monos, con_defs, type_intrs, type_elims);
   67.16  
   67.17  val ind_decl =
   67.18 -  (P.$$$ "domains" |-- P.!!! (P.enum1 "+" P.term --
   67.19 -      ((P.$$$ "\<subseteq>" || P.$$$ "<=") |-- P.term))) --
   67.20 -  (P.$$$ "intros" |--
   67.21 -    P.!!! (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- P.prop))) --
   67.22 -  Scan.optional (P.$$$ "monos" |-- P.!!! Parse_Spec.xthms1) [] --
   67.23 -  Scan.optional (P.$$$ "con_defs" |-- P.!!! Parse_Spec.xthms1) [] --
   67.24 -  Scan.optional (P.$$$ "type_intros" |-- P.!!! Parse_Spec.xthms1) [] --
   67.25 -  Scan.optional (P.$$$ "type_elims" |-- P.!!! Parse_Spec.xthms1) []
   67.26 +  (Parse.$$$ "domains" |-- Parse.!!! (Parse.enum1 "+" Parse.term --
   67.27 +      ((Parse.$$$ "\<subseteq>" || Parse.$$$ "<=") |-- Parse.term))) --
   67.28 +  (Parse.$$$ "intros" |--
   67.29 +    Parse.!!! (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop))) --
   67.30 +  Scan.optional (Parse.$$$ "monos" |-- Parse.!!! Parse_Spec.xthms1) [] --
   67.31 +  Scan.optional (Parse.$$$ "con_defs" |-- Parse.!!! Parse_Spec.xthms1) [] --
   67.32 +  Scan.optional (Parse.$$$ "type_intros" |-- Parse.!!! Parse_Spec.xthms1) [] --
   67.33 +  Scan.optional (Parse.$$$ "type_elims" |-- Parse.!!! Parse_Spec.xthms1) []
   67.34    >> (Toplevel.theory o mk_ind);
   67.35  
   67.36 -val _ = OuterSyntax.command (co_prefix ^ "inductive")
   67.37 -  ("define " ^ co_prefix ^ "inductive sets") K.thy_decl ind_decl;
   67.38 +val _ =
   67.39 +  Outer_Syntax.command (co_prefix ^ "inductive")
   67.40 +    ("define " ^ co_prefix ^ "inductive sets") Keyword.thy_decl ind_decl;
   67.41  
   67.42  end;
   67.43  
   67.44 -end;
   67.45 -
    68.1 --- a/src/ZF/Tools/primrec_package.ML	Mon May 17 15:11:25 2010 +0200
    68.2 +++ b/src/ZF/Tools/primrec_package.ML	Mon May 17 23:54:15 2010 +0200
    68.3 @@ -194,12 +194,11 @@
    68.4  
    68.5  (* outer syntax *)
    68.6  
    68.7 -structure P = OuterParse and K = OuterKeyword;
    68.8 -
    68.9  val _ =
   68.10 -  OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
   68.11 -    (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- P.prop)
   68.12 -      >> (Toplevel.theory o (#1 oo (add_primrec o map P.triple_swap))));
   68.13 +  Outer_Syntax.command "primrec" "define primitive recursive functions on datatypes"
   68.14 +    Keyword.thy_decl
   68.15 +    (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)
   68.16 +      >> (Toplevel.theory o (#1 oo (add_primrec o map Parse.triple_swap))));
   68.17  
   68.18  end;
   68.19  
    69.1 --- a/src/ZF/Tools/typechk.ML	Mon May 17 15:11:25 2010 +0200
    69.2 +++ b/src/ZF/Tools/typechk.ML	Mon May 17 23:54:15 2010 +0200
    69.3 @@ -118,7 +118,7 @@
    69.4      "ZF type-checking";
    69.5  
    69.6  val _ =
    69.7 -  OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag
    69.8 +  Outer_Syntax.improper_command "print_tcset" "print context of ZF typecheck" Keyword.diag
    69.9      (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
   69.10        Toplevel.keep (print_tcset o Toplevel.context_of)));
   69.11