1.1 --- a/doc-src/antiquote_setup.ML	Wed Jun 25 14:54:45 2008 +0200
     1.2 +++ b/doc-src/antiquote_setup.ML	Wed Jun 25 17:38:32 2008 +0200
     1.3 @@ -190,9 +190,9 @@
     1.4  
     1.5  val _ = O.add_commands
     1.6   (entity_antiqs no_check "" "syntax" @
     1.7 -  entity_antiqs (K (is_some o OuterSyntax.command_keyword)) "isacommand" "command" @
     1.8 -  entity_antiqs (K OuterSyntax.is_keyword) "isakeyword" "keyword" @
     1.9 -  entity_antiqs (K OuterSyntax.is_keyword) "isakeyword" "element" @
    1.10 +  entity_antiqs (K (is_some o OuterKeyword.command_keyword)) "isacommand" "command" @
    1.11 +  entity_antiqs (K OuterKeyword.is_keyword) "isakeyword" "keyword" @
    1.12 +  entity_antiqs (K OuterKeyword.is_keyword) "isakeyword" "element" @
    1.13    entity_antiqs (thy_check Method.intern Method.defined) "" "method" @
    1.14    entity_antiqs (thy_check Attrib.intern Attrib.defined) "" "attribute" @
    1.15    entity_antiqs no_check "" "fact" @

     2.1 --- a/src/HOL/Import/import_syntax.ML	Wed Jun 25 14:54:45 2008 +0200
     2.2 +++ b/src/HOL/Import/import_syntax.ML	Wed Jun 25 17:38:32 2008 +0200
     2.3 @@ -223,7 +223,7 @@
     2.4  val append_dump = (P.verbatim || P.string) >> add_dump
     2.5  
     2.6  fun setup () =
     2.7 -  (OuterSyntax.keywords[">"];
     2.8 +  (OuterKeyword.keyword ">";
     2.9     OuterSyntax.command "import_segment"
    2.10  		       "Set import segment name"
    2.11  		       K.thy_decl (import_segment >> Toplevel.theory);

     3.1 --- a/src/HOL/Import/proof_kernel.ML	Wed Jun 25 14:54:45 2008 +0200
     3.2 +++ b/src/HOL/Import/proof_kernel.ML	Wed Jun 25 17:38:32 2008 +0200
     3.3 @@ -190,7 +190,7 @@
     3.4    else Syntax.literal c
     3.5  
     3.6  fun quotename c =
     3.7 -  if Syntax.is_identifier c andalso not (OuterSyntax.is_keyword c) then c else quote c
     3.8 +  if Syntax.is_identifier c andalso not (OuterKeyword.is_keyword c) then c else quote c
     3.9  
    3.10  fun simple_smart_string_of_cterm ct =
    3.11      let

     4.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Wed Jun 25 14:54:45 2008 +0200
     4.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Jun 25 17:38:32 2008 +0200
     4.3 @@ -668,7 +668,7 @@
     4.4  
     4.5  local structure P = OuterParse and K = OuterKeyword in
     4.6  
     4.7 -val _ = OuterSyntax.keywords ["avoids"];
     4.8 +val _ = OuterKeyword.keyword "avoids";
     4.9  
    4.10  val _ =
    4.11    OuterSyntax.command "nominal_inductive"

     5.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Jun 25 14:54:45 2008 +0200
     5.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Jun 25 17:38:32 2008 +0200
     5.3 @@ -193,7 +193,7 @@
     5.4  
     5.5  local structure P = OuterParse and K = OuterKeyword in
     5.6  
     5.7 -val _ = OuterSyntax.keywords ["otherwise"];
     5.8 +val _ = OuterKeyword.keyword "otherwise";
     5.9  
    5.10  val _ =
    5.11    OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal

     6.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Jun 25 14:54:45 2008 +0200
     6.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Jun 25 17:38:32 2008 +0200
     6.3 @@ -932,7 +932,7 @@
     6.4  
     6.5  local structure P = OuterParse and K = OuterKeyword in
     6.6  
     6.7 -val _ = OuterSyntax.keywords ["monos"];
     6.8 +val _ = OuterKeyword.keyword "monos";
     6.9  
    6.10  fun flatten_specification specs = specs |> maps
    6.11    (fn (a, (concl, [])) => concl |> map

     7.1 --- a/src/HOL/Tools/recdef_package.ML	Wed Jun 25 14:54:45 2008 +0200
     7.2 +++ b/src/HOL/Tools/recdef_package.ML	Wed Jun 25 17:38:32 2008 +0200
     7.3 @@ -291,7 +291,7 @@
     7.4  
     7.5  local structure P = OuterParse and K = OuterKeyword in
     7.6  
     7.7 -val _ = OuterSyntax.keywords ["permissive", "congs", "hints"];
     7.8 +val _ = List.app OuterKeyword.keyword ["permissive", "congs", "hints"];
     7.9  
    7.10  val hints =
    7.11    P.$$$ "(" |-- P.!!! (P.position (P.$$$ "hints" -- P.arguments) --| P.$$$ ")") >> Args.src;

     8.1 --- a/src/HOL/Tools/typedef_package.ML	Wed Jun 25 14:54:45 2008 +0200
     8.2 +++ b/src/HOL/Tools/typedef_package.ML	Wed Jun 25 17:38:32 2008 +0200
     8.3 @@ -260,7 +260,7 @@
     8.4  
     8.5  local structure P = OuterParse and K = OuterKeyword in
     8.6  
     8.7 -val _ = OuterSyntax.keywords ["morphisms"];
     8.8 +val _ = OuterKeyword.keyword "morphisms";
     8.9  
    8.10  val typedef_decl =
    8.11    Scan.optional (P.$$$ "(" |--

     9.1 --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Wed Jun 25 14:54:45 2008 +0200
     9.2 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Wed Jun 25 17:38:32 2008 +0200
     9.3 @@ -485,7 +485,7 @@
     9.4  
     9.5  local structure P = OuterParse and K = OuterKeyword in
     9.6  
     9.7 -val _ = OuterSyntax.keywords ["signature", "actions", "inputs",
     9.8 +val _ = List.app OuterKeyword.keyword ["signature", "actions", "inputs",
     9.9    "outputs", "internals", "states", "initially", "transitions", "pre",
    9.10    "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
    9.11    "rename"];

    10.1 --- a/src/HOLCF/Tools/domain/domain_extender.ML	Wed Jun 25 14:54:45 2008 +0200
    10.2 +++ b/src/HOLCF/Tools/domain/domain_extender.ML	Wed Jun 25 17:38:32 2008 +0200
    10.3 @@ -146,7 +146,7 @@
    10.4  
    10.5  local structure P = OuterParse and K = OuterKeyword in
    10.6  
    10.7 -val _ = OuterSyntax.keywords ["lazy"];
    10.8 +val _ = OuterKeyword.keyword "lazy";
    10.9  
   10.10  val dest_decl =
   10.11    P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --

    11.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Jun 25 14:54:45 2008 +0200
    11.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Jun 25 17:38:32 2008 +0200
    11.3 @@ -16,7 +16,7 @@
    11.4  (*keep keywords consistent with the parsers, otherwise be prepared for
    11.5    unexpected errors*)
    11.6  
    11.7 -val _ = OuterSyntax.keywords
    11.8 +val _ = List.app OuterKeyword.keyword
    11.9   ["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
   11.10    "=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>",
   11.11    "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",

    12.1 --- a/src/Pure/Isar/outer_syntax.ML	Wed Jun 25 14:54:45 2008 +0200
    12.2 +++ b/src/Pure/Isar/outer_syntax.ML	Wed Jun 25 17:38:32 2008 +0200
    12.3 @@ -2,19 +2,16 @@
    12.4      ID:         $Id$
    12.5      Author:     Markus Wenzel, TU Muenchen
    12.6  
    12.7 -The global Isabelle/Isar outer syntax. Note: the syntax for files is
    12.8 -statically determined at the very beginning; for interactive processing
    12.9 -it may change dynamically.
   12.10 +The global Isabelle/Isar outer syntax.
   12.11 +
   12.12 +Note: the syntax for files is statically determined at the very
   12.13 +beginning; for interactive processing it may change dynamically.
   12.14  *)
   12.15  
   12.16  signature OUTER_SYNTAX =
   12.17  sig
   12.18    type parser_fn = OuterLex.token list ->
   12.19      (Toplevel.transition -> Toplevel.transition) * OuterLex.token list
   12.20 -  val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
   12.21 -  val command_keyword: string -> OuterKeyword.T option
   12.22 -  val is_keyword: string -> bool
   12.23 -  val keywords: string list -> unit
   12.24    val command: string -> string -> OuterKeyword.T -> parser_fn -> unit
   12.25    val markup_command: ThyOutput.markup -> string -> string -> OuterKeyword.T -> parser_fn -> unit
   12.26    val improper_command: string -> string -> OuterKeyword.T -> parser_fn -> unit
   12.27 @@ -24,11 +21,7 @@
   12.28      (OuterParse.token list -> (bool -> local_theory -> Proof.state) * OuterLex.token list) -> unit
   12.29    val local_theory_to_proof: string -> string -> OuterKeyword.T ->
   12.30      (OuterParse.token list -> (local_theory -> Proof.state) * OuterLex.token list) -> unit
   12.31 -  val dest_keywords: unit -> string list
   12.32 -  val dest_parsers: unit -> (string * string * string * bool) list
   12.33    val print_outer_syntax: unit -> unit
   12.34 -  val report: unit -> unit
   12.35 -  val check_text: string * Position.T -> Toplevel.node option -> unit
   12.36    val scan: string -> OuterLex.token list
   12.37    val parse: Position.T -> string -> Toplevel.transition list
   12.38    val process_file: Path.T -> theory -> theory
   12.39 @@ -46,30 +39,18 @@
   12.40  
   12.41  (** outer syntax **)
   12.42  
   12.43 -(* diagnostics *)
   12.44 -
   12.45 -fun report_keyword name =
   12.46 -  Pretty.mark (Markup.keyword_decl name)
   12.47 -    (Pretty.str ("Outer syntax keyword: " ^ quote name));
   12.48 -
   12.49 -fun report_command name kind =
   12.50 -  Pretty.mark (Markup.command_decl name kind)
   12.51 -    (Pretty.str ("Outer syntax command: " ^ quote name ^ " (" ^ kind ^ ")"));
   12.52 -
   12.53 -
   12.54  (* parsers *)
   12.55  
   12.56  type parser_fn = T.token list -> (Toplevel.transition -> Toplevel.transition) * T.token list;
   12.57  
   12.58  datatype parser = Parser of
   12.59   {comment: string,
   12.60 -  kind: OuterKeyword.T,
   12.61    markup: ThyOutput.markup option,
   12.62    int_only: bool,
   12.63    parse: parser_fn};
   12.64  
   12.65 -fun make_parser comment kind markup int_only parse =
   12.66 -  Parser {comment = comment, kind = kind, markup = markup, int_only = int_only, parse = parse};
   12.67 +fun make_parser comment markup int_only parse =
   12.68 +  Parser {comment = comment, markup = markup, int_only = int_only, parse = parse};
   12.69  
   12.70  
   12.71  (* parse command *)
   12.72 @@ -103,17 +84,9 @@
   12.73  
   12.74  local
   12.75  
   12.76 -val global_lexicons = ref (Scan.empty_lexicon, Scan.empty_lexicon);
   12.77  val global_parsers = ref (Symtab.empty: parser Symtab.table);
   12.78  val global_markups = ref ([]: (string * ThyOutput.markup) list);
   12.79  
   12.80 -fun change_lexicons f = CRITICAL (fn () =>
   12.81 -  let val lexs = f (! global_lexicons) in
   12.82 -    (case (op inter_string) (pairself Scan.dest_lexicon lexs) of
   12.83 -      [] => global_lexicons := lexs
   12.84 -    | bads => error ("Clash of outer syntax commands and keywords: " ^ commas_quote bads))
   12.85 -  end);
   12.86 -
   12.87  fun change_parsers f = CRITICAL (fn () =>
   12.88   (change global_parsers f;
   12.89    global_markups :=
   12.90 @@ -124,44 +97,30 @@
   12.91  
   12.92  (* access current syntax *)
   12.93  
   12.94 -fun get_lexicons () = CRITICAL (fn () => ! global_lexicons);
   12.95  fun get_parsers () = CRITICAL (fn () => ! global_parsers);
   12.96  fun get_markups () = CRITICAL (fn () => ! global_markups);
   12.97  
   12.98  fun get_parser () = Symtab.lookup (get_parsers ());
   12.99  
  12.100 -fun command_keyword name =
  12.101 -  (case Symtab.lookup (get_parsers ()) name of
  12.102 -    SOME (Parser {kind, ...}) => SOME kind
  12.103 -  | NONE => NONE);
  12.104 -
  12.105 -fun command_tags name = these (Option.map OuterKeyword.tags_of (command_keyword name));
  12.106 -
  12.107  fun is_markup kind name = AList.lookup (op =) (get_markups ()) name = SOME kind;
  12.108  
  12.109  
  12.110  (* augment syntax *)
  12.111  
  12.112 -fun keywords names =
  12.113 - (change_lexicons (apfst (Scan.extend_lexicon (map Symbol.explode names)));
  12.114 -  List.app (Pretty.writeln o report_keyword) names);
  12.115 -
  12.116 -
  12.117 -fun add_parser (name, parser as Parser {kind, ...}) =
  12.118 - (if not (Symtab.defined (get_parsers ()) name) then ()
  12.119 +fun add_parser name kind parser = CRITICAL (fn () =>
  12.120 + (OuterKeyword.command name kind;
  12.121 +  if not (Symtab.defined (get_parsers ()) name) then ()
  12.122    else warning ("Redefining outer syntax command " ^ quote name);
  12.123 -  change_parsers (Symtab.update (name, parser));
  12.124 -  change_lexicons (apsnd (Scan.extend_lexicon [Symbol.explode name]));
  12.125 -  Pretty.writeln (report_command name (OuterKeyword.kind_of kind)));
  12.126 +  change_parsers (Symtab.update (name, parser))));
  12.127  
  12.128  fun command name comment kind parse =
  12.129 -  add_parser (name, make_parser comment kind NONE false parse);
  12.130 +  add_parser name kind (make_parser comment NONE false parse);
  12.131  
  12.132  fun markup_command markup name comment kind parse =
  12.133 -  add_parser (name, make_parser comment kind (SOME markup) false parse);
  12.134 +  add_parser name kind (make_parser comment (SOME markup) false parse);
  12.135  
  12.136  fun improper_command name comment kind parse =
  12.137 -  add_parser (name, make_parser comment kind NONE true parse);
  12.138 +  add_parser name kind (make_parser comment NONE true parse);
  12.139  
  12.140  end;
  12.141  
  12.142 @@ -179,31 +138,22 @@
  12.143  
  12.144  (* inspect syntax *)
  12.145  
  12.146 -fun is_keyword s = Scan.is_literal (#1 (get_lexicons ())) (Symbol.explode s);
  12.147 -fun dest_keywords () = Scan.dest_lexicon (#1 (get_lexicons ()));
  12.148 -
  12.149  fun dest_parsers () =
  12.150    get_parsers () |> Symtab.dest |> sort_wrt #1
  12.151 -  |> map (fn (name, Parser {comment, kind, int_only, ...}) =>
  12.152 -    (name, comment, OuterKeyword.kind_of kind, int_only));
  12.153 +  |> map (fn (name, Parser {comment, int_only, ...}) => (name, comment, int_only));
  12.154  
  12.155  fun print_outer_syntax () =
  12.156    let
  12.157 -    fun pretty_cmd (name, comment, _, _) =
  12.158 +    fun pretty_cmd (name, comment, _) =
  12.159        Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
  12.160 -    val (int_cmds, cmds) = List.partition #4 (dest_parsers ());
  12.161 +    val (int_cmds, cmds) = List.partition #3 (dest_parsers ());
  12.162    in
  12.163 -    [Pretty.strs ("syntax keywords:" :: map quote (dest_keywords ())),
  12.164 +    [Pretty.strs ("syntax keywords:" :: map quote (OuterKeyword.dest_keywords ())),
  12.165        Pretty.big_list "commands:" (map pretty_cmd cmds),
  12.166        Pretty.big_list "interactive-only commands:" (map pretty_cmd int_cmds)]
  12.167      |> Pretty.chunks |> Pretty.writeln
  12.168    end;
  12.169  
  12.170 -fun report () =
  12.171 -  (map report_keyword (dest_keywords ()) @
  12.172 -    map (fn (name, _, kind, _) => report_command name kind) (dest_parsers ()))
  12.173 -  |> Pretty.chunks |> Pretty.writeln;
  12.174 -
  12.175  
  12.176  
  12.177  (** toplevel parsing **)
  12.178 @@ -235,13 +185,13 @@
  12.179  fun scan str =
  12.180    Source.of_string str
  12.181    |> Symbol.source false
  12.182 -  |> T.source (SOME false) get_lexicons Position.none
  12.183 +  |> T.source (SOME false) OuterKeyword.get_lexicons Position.none
  12.184    |> Source.exhaust;
  12.185  
  12.186  fun parse pos str =
  12.187    Source.of_string str
  12.188    |> Symbol.source false
  12.189 -  |> T.source (SOME false) get_lexicons pos
  12.190 +  |> T.source (SOME false) OuterKeyword.get_lexicons pos
  12.191    |> toplevel_source false NONE get_parser
  12.192    |> Source.exhaust;
  12.193  
  12.194 @@ -268,37 +218,30 @@
  12.195  fun isar term : isar =
  12.196    Source.tty
  12.197    |> Symbol.source true
  12.198 -  |> T.source (SOME true) get_lexicons Position.none
  12.199 +  |> T.source (SOME true) OuterKeyword.get_lexicons Position.none
  12.200    |> toplevel_source term (SOME true) get_parser;
  12.201  
  12.202  
  12.203 -
  12.204 -(** read theory **)
  12.205 -
  12.206 -(* check_text *)
  12.207 -
  12.208 -fun check_text s state = (ThyOutput.eval_antiquote (#1 (get_lexicons ())) state s; ());
  12.209 -
  12.210 -
  12.211  (* load_thy *)
  12.212  
  12.213  fun load_thy dir name pos text time =
  12.214    let
  12.215      val text_src = Source.of_list (Library.untabify text);
  12.216 +    val (lexs, parser) = CRITICAL (fn () => (OuterKeyword.get_lexicons (), get_parser ()));
  12.217  
  12.218      val _ = Present.init_theory name;
  12.219      val _ = Present.verbatim_source name (fn () => Source.exhaust (Symbol.source false text_src));
  12.220      val toks = text_src
  12.221        |> Symbol.source false
  12.222 -      |> T.source NONE (K (get_lexicons ())) pos
  12.223 +      |> T.source NONE (K lexs) pos
  12.224        |> Source.exhausted;
  12.225      val trs = toks
  12.226 -      |> toplevel_source false NONE (K (get_parser ()))
  12.227 +      |> toplevel_source false NONE (K parser)
  12.228        |> Source.exhaust;
  12.229  
  12.230      val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
  12.231      val _ = cond_timeit time "" (fn () =>
  12.232 -      ThyOutput.process_thy (#1 (get_lexicons ())) command_tags is_markup trs toks
  12.233 +      ThyOutput.process_thy (#1 lexs) OuterKeyword.command_tags is_markup trs toks
  12.234        |> Buffer.content
  12.235        |> Present.theory_output name);
  12.236      val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();

    13.1 --- a/src/Pure/ProofGeneral/pgip_parser.ML	Wed Jun 25 14:54:45 2008 +0200
    13.2 +++ b/src/Pure/ProofGeneral/pgip_parser.ML	Wed Jun 25 17:38:32 2008 +0200
    13.3 @@ -83,7 +83,7 @@
    13.4  
    13.5  fun parse_command "sorry" text = [D.Postponegoal {text = text}, D.Closeblock {}]
    13.6    | parse_command name text =
    13.7 -      (case OuterSyntax.command_keyword name of
    13.8 +      (case OuterKeyword.command_keyword name of
    13.9          NONE => [D.Unparseable {text = text}]
   13.10        | SOME k =>
   13.11            (case Symtab.lookup command_keywords (OuterKeyword.kind_of k) of

    14.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Jun 25 14:54:45 2008 +0200
    14.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Jun 25 17:38:32 2008 +0200
    14.3 @@ -359,16 +359,15 @@
    14.4  (** lexicalstructure element with keywords (PGIP version of elisp keywords file) **)
    14.5  
    14.6  fun lexicalstructure_keywords () =
    14.7 -    let val commands = OuterSyntax.dest_keywords ()
    14.8 -        fun category_of k = if k mem commands then "major" else "minor"
    14.9 -         (* NB: we might filter to only include words like elisp case (OuterSyntax.is_keyword). *)
   14.10 -        fun keyword_elt (keyword,help,kind,_) =
   14.11 -            XML.Elem("keyword", [("word", keyword), ("category", category_of kind)],
   14.12 -                     [XML.Elem("shorthelp", [], [XML.Text help])])
   14.13 +    let val keywords = OuterKeyword.dest_keywords ()
   14.14 +        val commands = OuterKeyword.dest_commands ()
   14.15 +        fun keyword_elt kind keyword =
   14.16 +            XML.Elem("keyword", [("word", keyword), ("category", kind)], [])
   14.17          in
   14.18              (* Also, note we don't call init_outer_syntax here to add interface commands,
   14.19              but they should never appear in scripts anyway so it shouldn't matter *)
   14.20 -            Lexicalstructure {content = map keyword_elt (OuterSyntax.dest_parsers()) }
   14.21 +            Lexicalstructure
   14.22 +              {content = map (keyword_elt "minor") keywords @ map (keyword_elt "major") commands}
   14.23          end
   14.24  
   14.25  (* TODO: we can issue a lexicalstructure/keyword when the syntax gets extended dynamically;

    15.1 --- a/src/Pure/Thy/thy_edit.ML	Wed Jun 25 14:54:45 2008 +0200
    15.2 +++ b/src/Pure/Thy/thy_edit.ML	Wed Jun 25 17:38:32 2008 +0200
    15.3 @@ -35,7 +35,7 @@
    15.4  
    15.5  fun token_source pos src =
    15.6    Symbol.source true src
    15.7 -  |> T.source (SOME false) OuterSyntax.get_lexicons pos;
    15.8 +  |> T.source (SOME false) OuterKeyword.get_lexicons pos;
    15.9  
   15.10  fun parse_tokens pos src = Source.exhaust (token_source pos src);
   15.11  

    16.1 --- a/src/Pure/codegen.ML	Wed Jun 25 14:54:45 2008 +0200
    16.2 +++ b/src/Pure/codegen.ML	Wed Jun 25 17:38:32 2008 +0200
    16.3 @@ -1111,7 +1111,7 @@
    16.4  
    16.5  structure P = OuterParse and K = OuterKeyword;
    16.6  
    16.7 -val _ = OuterSyntax.keywords ["attach", "file", "contains"];
    16.8 +val _ = List.app OuterKeyword.keyword ["attach", "file", "contains"];
    16.9  
   16.10  fun strip_whitespace s = implode (fst (take_suffix (equal "\n" orf equal " ")
   16.11    (snd (take_prefix (equal "\n" orf equal " ") (explode s))))) ^ "\n";

    17.1 --- a/src/Tools/code/code_target.ML	Wed Jun 25 14:54:45 2008 +0200
    17.2 +++ b/src/Tools/code/code_target.ML	Wed Jun 25 17:38:32 2008 +0200
    17.3 @@ -2216,7 +2216,7 @@
    17.4       -- Scan.optional (P.$$$ "(" |-- P.arguments --| P.$$$ ")") []
    17.5    ) >> (fn (raw_cs, seris) => cmd raw_cs seris));
    17.6  
    17.7 -val _ = OuterSyntax.keywords [infixK, infixlK, infixrK, inK, module_nameK, fileK];
    17.8 +val _ = List.app OuterKeyword.keyword [infixK, infixlK, infixrK, inK, module_nameK, fileK];
    17.9  
   17.10  val _ =
   17.11    OuterSyntax.command "code_class" "define code syntax for class" K.thy_decl (

    18.1 --- a/src/ZF/Tools/induct_tacs.ML	Wed Jun 25 14:54:45 2008 +0200
    18.2 +++ b/src/ZF/Tools/induct_tacs.ML	Wed Jun 25 17:38:32 2008 +0200
    18.3 @@ -188,7 +188,7 @@
    18.4  
    18.5  local structure P = OuterParse and K = OuterKeyword in
    18.6  
    18.7 -val _ = OuterSyntax.keywords ["elimination", "induction", "case_eqns", "recursor_eqns"];
    18.8 +val _ = List.app OuterKeyword.keyword ["elimination", "induction", "case_eqns", "recursor_eqns"];
    18.9  
   18.10  val rep_datatype_decl =
   18.11    (P.$$$ "elimination" |-- P.!!! SpecParse.xthm) --