# HG changeset patch
# User wenzelm
# Date 1191682204 -7200
# Node ID e5b55d7be9bb6c2be0b0b56bcb94b6c0c1a1d4cb
# Parent  6e6d9e80ebb46df569ec960c907b16a8877b0f31
simplified interfaces for outer syntax;

diff -r 6e6d9e80ebb4 -r e5b55d7be9bb NEWS
--- a/NEWS	Sat Oct 06 16:41:22 2007 +0200
+++ b/NEWS	Sat Oct 06 16:50:04 2007 +0200
@@ -1337,6 +1337,11 @@
 quasi-functional intermediate checkpoint, both in interactive and
 batch mode.
 
+* Isar: simplified interfaces for outer syntax.  Renamed
+OuterSyntax.add_keywords to OuterSyntax.keywords.  Removed
+OuterSyntax.add_parsers -- this functionality is now included in
+OuterSyntax.command etc.  INCOMPATIBILITY.
+
 * Simplifier: the simpset of a running simplification process now
 contains a proof context (cf. Simplifier.the_context), which is the
 very context that the initial simpset has been retrieved from (by
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/HOL/Import/import_syntax.ML
--- a/src/HOL/Import/import_syntax.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Import/import_syntax.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -5,7 +5,7 @@
 
 signature HOL4_IMPORT_SYNTAX =
 sig
-    type token = OuterSyntax.token
+    type token = OuterLex.token
     type command  = token list -> (theory -> theory) * token list 
 
     val import_segment: token list -> (theory -> theory) * token list
@@ -32,7 +32,7 @@
 structure HOL4ImportSyntax :> HOL4_IMPORT_SYNTAX =
 struct
 
-type token = OuterSyntax.token
+type token = OuterLex.token
 type command  = token list -> (theory -> theory) * token list 
 
 local structure P = OuterParse and K = OuterKeyword in
@@ -222,61 +222,59 @@
 fun fl_dump toks  = Scan.succeed flush_dump toks
 val append_dump = (P.verbatim || P.string) >> add_dump
 
-val parsers = 
-  [OuterSyntax.command "import_segment"
+fun setup () =
+  (OuterSyntax.keywords[">"];
+   OuterSyntax.command "import_segment"
 		       "Set import segment name"
-		       K.thy_decl (import_segment >> Toplevel.theory),
+		       K.thy_decl (import_segment >> Toplevel.theory);
    OuterSyntax.command "import_theory"
 		       "Set default HOL4 theory name"
-		       K.thy_decl (import_theory >> Toplevel.theory),
+		       K.thy_decl (import_theory >> Toplevel.theory);
    OuterSyntax.command "end_import"
 		       "End HOL4 import"
-		       K.thy_decl (end_import >> Toplevel.theory),
+		       K.thy_decl (end_import >> Toplevel.theory);
    OuterSyntax.command "skip_import_dir" 
                        "Sets caching directory for skipping importing"
-                       K.thy_decl (skip_import_dir >> Toplevel.theory),
+                       K.thy_decl (skip_import_dir >> Toplevel.theory);
    OuterSyntax.command "skip_import" 
                        "Switches skipping importing on or off"
-                       K.thy_decl (skip_import >> Toplevel.theory),		      
+                       K.thy_decl (skip_import >> Toplevel.theory);		      
    OuterSyntax.command "setup_theory"
 		       "Setup HOL4 theory replaying"
-		       K.thy_decl (setup_theory >> Toplevel.theory),
+		       K.thy_decl (setup_theory >> Toplevel.theory);
    OuterSyntax.command "end_setup"
 		       "End HOL4 setup"
-		       K.thy_decl (end_setup >> Toplevel.theory),
+		       K.thy_decl (end_setup >> Toplevel.theory);
    OuterSyntax.command "setup_dump"
 		       "Setup the dump file name"
-		       K.thy_decl (set_dump >> Toplevel.theory),
+		       K.thy_decl (set_dump >> Toplevel.theory);
    OuterSyntax.command "append_dump"
 		       "Add text to dump file"
-		       K.thy_decl (append_dump >> Toplevel.theory),
+		       K.thy_decl (append_dump >> Toplevel.theory);
    OuterSyntax.command "flush_dump"
 		       "Write the dump to file"
-		       K.thy_decl (fl_dump >> Toplevel.theory),
+		       K.thy_decl (fl_dump >> Toplevel.theory);
    OuterSyntax.command "ignore_thms"
 		       "Theorems to ignore in next HOL4 theory import"
-		       K.thy_decl (ignore_thms >> Toplevel.theory),
+		       K.thy_decl (ignore_thms >> Toplevel.theory);
    OuterSyntax.command "type_maps"
 		       "Map HOL4 type names to existing Isabelle/HOL type names"
-		       K.thy_decl (type_maps >> Toplevel.theory),
+		       K.thy_decl (type_maps >> Toplevel.theory);
    OuterSyntax.command "def_maps"
 		       "Map HOL4 constant names to their primitive definitions"
-		       K.thy_decl (def_maps >> Toplevel.theory),
+		       K.thy_decl (def_maps >> Toplevel.theory);
    OuterSyntax.command "thm_maps"
 		       "Map HOL4 theorem names to existing Isabelle/HOL theorem names"
-		       K.thy_decl (thm_maps >> Toplevel.theory),
+		       K.thy_decl (thm_maps >> Toplevel.theory);
    OuterSyntax.command "const_renames"
 		       "Rename HOL4 const names"
-		       K.thy_decl (const_renames >> Toplevel.theory),
+		       K.thy_decl (const_renames >> Toplevel.theory);
    OuterSyntax.command "const_moves"
 		       "Rename HOL4 const names to other HOL4 constants"
-		       K.thy_decl (const_moves >> Toplevel.theory),
+		       K.thy_decl (const_moves >> Toplevel.theory);
    OuterSyntax.command "const_maps"
 		       "Map HOL4 const names to existing Isabelle/HOL const names"
-		       K.thy_decl (const_maps >> Toplevel.theory)]
-
-fun setup () = (OuterSyntax.add_keywords[">"];
-		OuterSyntax.add_parsers parsers)
+		       K.thy_decl (const_maps >> Toplevel.theory));
 
 end
 
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/HOL/Library/Eval.thy
--- a/src/HOL/Library/Eval.thy	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Library/Eval.thy	Sat Oct 06 16:50:04 2007 +0200
@@ -213,14 +213,11 @@
 *}
 
 ML {*
-val valueP =
   OuterSyntax.improper_command "value" "read, evaluate and print term" OuterKeyword.diag
     (Scan.option (OuterParse.$$$ "(" |-- OuterParse.name --| OuterParse.$$$ ")")
     -- OuterParse.term
       >> (fn (some_name, t) => Toplevel.no_timing o Toplevel.keep
            (Eval.evaluate_cmd some_name t)));
-
-val _ = OuterSyntax.add_parsers [valueP];
 *}
 
 end
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -947,10 +947,8 @@
 (* syntax und parsing *)
 structure P = OuterParse and K = OuterKeyword;
 
-val atom_declP =
+val _ =
   OuterSyntax.command "atom_decl" "Declare new kinds of atoms" K.thy_decl
     (Scan.repeat1 P.name >> (Toplevel.theory o create_nom_typedecls));
 
-val _ = OuterSyntax.add_parsers [atom_declP];
-
 end;
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -511,22 +511,21 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
-val nominal_inductiveP =
+val _ = OuterSyntax.keywords ["avoids"];
+
+val _ =
   OuterSyntax.command "nominal_inductive"
     "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal
     (P.name -- Scan.optional (P.$$$ "avoids" |-- P.and_list1 (P.name --
       (P.$$$ ":" |-- Scan.repeat1 P.name))) [] >> (fn (name, avoids) =>
         Toplevel.print o Toplevel.theory_to_proof (prove_strong_ind name avoids)));
 
-val equivarianceP =
+val _ =
   OuterSyntax.command "equivariance"
     "prove equivariance for inductive predicate involving nominal datatypes" K.thy_decl
     (P.name -- Scan.optional (P.$$$ "[" |-- P.list1 P.name --| P.$$$ "]") [] >>
       (fn (name, atoms) => Toplevel.theory (prove_eqvt name atoms)));
 
-val _ = OuterSyntax.add_keywords ["avoids"];
-val _ = OuterSyntax.add_parsers [nominal_inductiveP, equivarianceP];
-
 end;
 
 end
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -2094,12 +2094,10 @@
       (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
   in add_nominal_datatype false names specs end;
 
-val nominal_datatypeP =
+val _ =
   OuterSyntax.command "nominal_datatype" "define inductive datatypes" K.thy_decl
     (P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
 
-val _ = OuterSyntax.add_parsers [nominal_datatypeP];
-
 end;
 
 end
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -416,6 +416,8 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
+val _ = OuterSyntax.keywords ["invariant", "freshness_context"];
+
 val parser1 = P.$$$ "freshness_context" |-- P.$$$ ":" |-- (P.term >> SOME);
 val parser2 =
   P.$$$ "invariant" |-- P.$$$ ":" |--
@@ -434,16 +436,13 @@
 val primrec_decl =
   options -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
 
-val primrecP =
+val _ =
   OuterSyntax.command "nominal_primrec" "define primitive recursive functions on nominal datatypes" K.thy_goal
     (primrec_decl >> (fn ((unchecked, (alt_name, (invs, fctxt))), eqns) =>
       Toplevel.print o Toplevel.theory_to_proof
         ((if unchecked then add_primrec_unchecked else add_primrec) alt_name invs fctxt
           (map P.triple_swap eqns))));
 
-val _ = OuterSyntax.add_parsers [primrecP];
-val _ = OuterSyntax.add_keywords ["invariant", "freshness_context"];
-
 end;
 
 
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Orderings.thy	Sat Oct 06 16:50:04 2007 +0200
@@ -346,7 +346,7 @@
     (Context.cases (print_structures o ProofContext.init) print_structures)
     (print_structures o Proof.context_of));
 
-val printP =
+val _ =
   OuterSyntax.improper_command "print_orders"
     "print order structures available to transitivity reasoner" OuterKeyword.diag
     (Scan.succeed (Toplevel.no_timing o print));
@@ -354,11 +354,10 @@
 
 (** Setup **)
 
-val setup = let val _ = OuterSyntax.add_parsers [printP] in
-    Method.add_methods [("order", Method.ctxt_args (Method.SIMPLE_METHOD' o order_tac []),
-      "normalisation of algebraic structure")] #>
-    Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")]
-  end;
+val setup =
+  Method.add_methods
+    [("order", Method.ctxt_args (Method.SIMPLE_METHOD' o order_tac []), "transitivity reasoner")] #>
+  Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")];
 
 end;
 
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -908,6 +908,8 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
+val _ = OuterSyntax.keywords ["distinct", "inject", "induction"];
+
 val datatype_decl =
   Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --
     (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
@@ -919,7 +921,7 @@
       (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
   in snd o add_datatype false names specs end;
 
-val datatypeP =
+val _ =
   OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl
     (P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
 
@@ -932,14 +934,10 @@
 
 fun mk_rep_datatype (((opt_ts, dss), iss), ind) = #2 o rep_datatype opt_ts dss iss ind;
 
-val rep_datatypeP =
+val _ =
   OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_decl
     (rep_datatype_decl >> (Toplevel.theory o mk_rep_datatype));
 
-
-val _ = OuterSyntax.add_keywords ["distinct", "inject", "induction"];
-val _ = OuterSyntax.add_parsers [datatypeP, rep_datatypeP];
-
 end;
 
 
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/HOL/Tools/function_package/fundef_datatype.ML
--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -302,13 +302,12 @@
       |> by_pat_completeness_simp
       |> termination_by_lexicographic_order
 
-val funP =
+val _ =
   OuterSyntax.command "fun" "define general recursive functions (short version)" K.thy_decl
   (fundef_parser fun_config
      >> (fn ((config, fixes), (flags, statements)) =>
             (Toplevel.local_theory (target_of config) (fun_cmd config fixes statements flags))));
 
-val _ = OuterSyntax.add_parsers [funP];
 end
 
 end
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -268,24 +268,22 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
-val functionP =
+val _ = OuterSyntax.keywords ["sequential", "otherwise"];
+
+val _ =
   OuterSyntax.command "function" "define general recursive functions" K.thy_goal
   (fundef_parser default_config
      >> (fn ((config, fixes), (flags, statements)) =>
             Toplevel.local_theory_to_proof (target_of config) (add_fundef fixes statements config flags)
             #> Toplevel.print));
 
-val terminationP =
+val _ =
   OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
   (P.opt_target -- Scan.option P.term
     >> (fn (target, name) =>
            Toplevel.print o
            Toplevel.local_theory_to_proof target (setup_termination_proof name)));
 
-val _ = OuterSyntax.add_parsers [functionP];
-val _ = OuterSyntax.add_parsers [terminationP];
-val _ = OuterSyntax.add_keywords ["sequential", "otherwise"];
-
 end;
 
 
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -923,6 +923,8 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
+val _ = OuterSyntax.keywords ["monos"];
+
 (* FIXME tmp *)
 fun flatten_specification specs = specs |> maps
   (fn (a, (concl, [])) => concl |> map
@@ -945,22 +947,15 @@
 
 val ind_decl = gen_ind_decl add_ind_def;
 
-val inductiveP =
-  OuterSyntax.command "inductive" "define inductive predicates" K.thy_decl (ind_decl false);
+val _ = OuterSyntax.command "inductive" "define inductive predicates" K.thy_decl (ind_decl false);
+val _ = OuterSyntax.command "coinductive" "define coinductive predicates" K.thy_decl (ind_decl true);
 
-val coinductiveP =
-  OuterSyntax.command "coinductive" "define coinductive predicates" K.thy_decl (ind_decl true);
-
-
-val inductive_casesP =
+val _ =
   OuterSyntax.command "inductive_cases"
     "create simplified instances of elimination rules (improper)" K.thy_script
     (P.opt_target -- P.and_list1 SpecParse.spec
       >> (fn (loc, specs) => Toplevel.local_theory loc (snd o inductive_cases specs)));
 
-val _ = OuterSyntax.add_keywords ["monos"];
-val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];
-
 end;
 
 end;
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/HOL/Tools/inductive_set_package.ML
--- a/src/HOL/Tools/inductive_set_package.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Tools/inductive_set_package.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -543,14 +543,12 @@
 
 val ind_set_decl = InductivePackage.gen_ind_decl add_ind_set_def;
 
-val inductive_setP =
+val _ =
   OuterSyntax.command "inductive_set" "define inductive sets" K.thy_decl (ind_set_decl false);
 
-val coinductive_setP =
+val _ =
   OuterSyntax.command "coinductive_set" "define coinductive sets" K.thy_decl (ind_set_decl true);
 
-val _ = OuterSyntax.add_parsers [inductive_setP, coinductive_setP];
-
 end;
 
 end;
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Tools/primrec_package.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -350,15 +350,13 @@
 val primrec_decl =
   opt_unchecked_name -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
 
-val primrecP =
+val _ =
   OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
     (primrec_decl >> (fn ((unchecked, alt_name), eqns) =>
       Toplevel.theory (snd o
         (if unchecked then add_primrec_unchecked else add_primrec) alt_name
           (map P.triple_swap eqns))));
 
-val _ = OuterSyntax.add_parsers [primrecP];
-
 end;
 
 end;
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -295,6 +295,8 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
+val _ = OuterSyntax.keywords ["permissive", "congs", "hints"];
+
 val hints =
   P.$$$ "(" |-- P.!!! (P.position (P.$$$ "hints" -- P.arguments) --| P.$$$ ")") >> Args.src;
 
@@ -303,7 +305,7 @@
   P.name -- P.term -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop) -- Scan.option hints
   >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
 
-val recdefP =
+val _ =
   OuterSyntax.command "recdef" "define general recursive functions (TFL)" K.thy_decl
     (recdef_decl >> Toplevel.theory);
 
@@ -313,21 +315,17 @@
   Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (SpecParse.xthms1 --| P.$$$ ")")) []
   >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
 
-val defer_recdefP =
+val _ =
   OuterSyntax.command "defer_recdef" "defer general recursive functions (TFL)" K.thy_decl
     (defer_recdef_decl >> Toplevel.theory);
 
-val recdef_tcP =
+val _ =
   OuterSyntax.command "recdef_tc" "recommence proof of termination condition (TFL)" K.thy_goal
     (P.opt_target --
       SpecParse.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
       >> (fn (((loc, thm_name), name), i) =>
         Toplevel.print o Toplevel.local_theory_to_proof' loc (recdef_tc thm_name name i)));
 
-
-val _ = OuterSyntax.add_keywords ["permissive", "congs", "hints"];
-val _ = OuterSyntax.add_parsers [recdefP, defer_recdefP, recdef_tcP];
-
 end;
 
 end;
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Tools/record_package.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -607,7 +607,7 @@
                        val types = map snd flds';
                        val (args,rest) = splitargs (map fst flds') fargs;
                        val argtypes = map (Sign.certify_typ thy o decode_type thy) args;
-                       val midx =  fold (fn T => fn i => Int.max (maxidx_of_typ T, i)) 
+                       val midx =  fold (fn T => fn i => Int.max (maxidx_of_typ T, i))
                                     argtypes 0;
                        val varifyT = varifyT midx;
                        val vartypes = map varifyT types;
@@ -654,12 +654,12 @@
       gen_adv_record_type_scheme_tr "_field_types" "_field_type" ext_typeN;
 
 
-val parse_translation = 
+val parse_translation =
  [("_record_update", record_update_tr),
   ("_update_name", update_name_tr)];
 
 
-val adv_parse_translation = 
+val adv_parse_translation =
  [("_record",adv_record_tr),
   ("_record_scheme",adv_record_scheme_tr),
   ("_record_type",adv_record_type_tr),
@@ -762,7 +762,7 @@
           in Syntax.term_of_typ (! Syntax.show_sorts)
                (Sign.extern_typ thy (Envir.norm_type subst abbrT)) end;
 
-      fun match rT T = (Sign.typ_match thy (varifyT rT,T) 
+      fun match rT T = (Sign.typ_match thy (varifyT rT,T)
                                                 Vartab.empty);
 
    in if !print_record_type_abbr
@@ -876,8 +876,8 @@
      val f_x = Free (f',fT)$(Free (x,T'));
      fun is_constr (Const (c,_)$_) = can (unsuffix extN) c
        | is_constr _ = false;
-     fun subst (t as u$w) = if Free (f',fT)=u 
-                            then if is_constr w then f_x 
+     fun subst (t as u$w) = if Free (f',fT)=u
+                            then if is_constr w then f_x
                                  else raise TERM ("abstract_over_fun_app",[t])
                             else subst u$subst w
        | subst (Abs (x,T,t)) = (Abs (x,T,subst t))
@@ -885,12 +885,12 @@
      val t'' = abstract_over (f_x,subst t');
      val vars = strip_qnt_vars "all" t'';
      val bdy = strip_qnt_body "all" t'';
-     
+
   in list_abs ((x,T')::vars,bdy) end
   | abstract_over_fun_app t = raise TERM ("abstract_over_fun_app",[t]);
 (* Generates a theorem of the kind:
- * !!f x*. PROP P (f ( r x* ) x* == !!r x*. PROP P r x* 
- *) 
+ * !!f x*. PROP P (f ( r x* ) x* == !!r x*. PROP P r x*
+ *)
 fun mk_fun_apply_eq (Abs (f, fT, t)) thy =
   let
     val rT = domain_type fT;
@@ -900,16 +900,16 @@
     fun app_bounds 0 t = t$Bound 0
       | app_bounds n t = if n > 0 then app_bounds (n-1) (t$Bound n) else t
 
-   
+
     val [P,r] = Term.variant_frees t [("P",rT::Ts--->Term.propT),("r",Ts--->rT)];
     val prop = Logic.mk_equals
                 (list_all ((f,fT)::vars,
                            app_bounds (n - 1) ((Free P)$(Bound n$app_bounds (n-1) (Free r)))),
                  list_all ((fst r,rT)::vars,
-                           app_bounds (n - 1) ((Free P)$Bound n))); 
+                           app_bounds (n - 1) ((Free P)$Bound n)));
     val prove_standard = quick_and_dirty_prove true thy;
     val thm = prove_standard [] prop (fn prems =>
-	 EVERY [rtac equal_intr_rule 1, 
+	 EVERY [rtac equal_intr_rule 1,
                 Goal.norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1,
                 Goal.norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1]);
   in thm end
@@ -928,14 +928,14 @@
                   (trm as Abs _) =>
          (case rec_id (~1) T of
             "" => NONE
-          | n => if T=T'  
+          | n => if T=T'
                  then (let
-                        val P=cterm_of thy (abstract_over_fun_app trm); 
+                        val P=cterm_of thy (abstract_over_fun_app trm);
                         val thm = mk_fun_apply_eq trm thy;
                         val PV = cterm_of thy (hd (term_vars (prop_of thm)));
                         val thm' = cterm_instantiate [(PV,P)] thm;
                        in SOME  thm' end handle TERM _ => NONE)
-                else NONE) 
+                else NONE)
        | _ => NONE))
 end
 
@@ -951,7 +951,7 @@
                               (* [thm] is the same as all_thm *)
                  | NONE => extsplits)
     val thms'=K_comp_convs@thms;
-    val ss' = (Simplifier.inherit_context ss simpset 
+    val ss' = (Simplifier.inherit_context ss simpset
                 addsimps thms'
                 addsimprocs [record_split_f_more_simproc]);
   in
@@ -992,8 +992,8 @@
                      NONE => NONE
                    | SOME u_name
                      => if u_name = s
-                        then (case mk_eq_terms r of 
-                               NONE => 
+                        then (case mk_eq_terms r of
+                               NONE =>
                                  let
                                    val rv = ("r",rT)
                                    val rb = Bound 0
@@ -1064,7 +1064,7 @@
                         in ((Const (u,uT)$k$sprout,Const (u,uT)$kb$skeleton),kv::vars) end
                    else ((sprout,skeleton),vars);
 
-             fun is_upd_same (sprout,skeleton) u 
+             fun is_upd_same (sprout,skeleton) u
                                 ((K_rec as Const ("Record.K_record",_))$
                                   ((sel as Const (s,_))$r)) =
                    if (unsuffix updateN u) = s andalso (seed s sprout) = r
@@ -1074,17 +1074,17 @@
 
              fun init_seed r = ((r,Bound 0), [("r", rT)]);
 
-             fun add (n:string) f fmaps = 
+             fun add (n:string) f fmaps =
                (case AList.lookup (op =) fmaps n of
                   NONE => AList.update (op =) (n,[f]) fmaps
-                | SOME fs => AList.update (op =) (n,f::fs) fmaps) 
+                | SOME fs => AList.update (op =) (n,f::fs) fmaps)
 
-             fun comps (n:string) T fmaps = 
+             fun comps (n:string) T fmaps =
                (case AList.lookup (op =) fmaps n of
-                 SOME fs => 
+                 SOME fs =>
                    foldr1 (fn (f,g) => Const ("Fun.comp",(T-->T)-->(T-->T)-->(T-->T))$f$g) fs
                 | NONE => error ("record_upd_simproc.comps"))
-             
+
              (* mk_updterm returns either
               *  - Init (orig-term, orig-term-skeleton, vars) if no optimisation can be made,
               *     where vars are the bound variables in the skeleton
@@ -1119,7 +1119,7 @@
                                    val kv = (n, kT);
                                    val kb = Bound (length vars);
                                    val (sprout',vars') = grow u uT k kT (kv::vars) sprout;
-                                 in Inter(upd$kb$trm,trm',kv::vars',add n kb fmaps,sprout') 
+                                 in Inter(upd$kb$trm,trm',kv::vars',add n kb fmaps,sprout')
                                  end)
                          else
                           (case rest (u::already) r of
@@ -1149,7 +1149,7 @@
                                     val kv = (n, kT)
                                     val kb = Bound (length vars)
                                     val (sprout',vars') = grow u uT k kT (kv::vars) sprout
-                                    val fmaps' = add n kb fmaps 
+                                    val fmaps' = add n kb fmaps
                                   in Inter (upd$kb$trm,upd$comps n T fmaps'$trm'
                                            ,vars',fmaps',sprout') end))
                      end
@@ -1161,7 +1161,7 @@
                 => SOME (prove_split_simp thy ss rT
                           (list_all(vars,(equals rT$trm$trm'))))
              | _ => NONE)
-         end 
+         end
        | _ => NONE))
 end
 
@@ -1625,7 +1625,7 @@
         val refls = map mkrefl fields_more;
         val dest_convs' = map mk_meta_eq dest_convs;
         val map_eqs = map (uncurry Thm.combination) (refls ~~ dest_convs');
-        
+
         val constr_refl = Thm.reflexive (cterm_of defs_thy (head_of ext));
 
         fun mkthm (udef,(fld_refl,thms)) =
@@ -1664,7 +1664,7 @@
     val split_meta = timeit_msg "record extension split_meta proof:" split_meta_prf;
 
 
-    val (([inject',induct',cases',surjective',split_meta'], 
+    val (([inject',induct',cases',surjective',split_meta'],
           [dest_convs',upd_convs']),
       thm_thy) =
       defs_thy
@@ -1915,7 +1915,7 @@
       ||>> ((PureThy.add_defs_i false o map Thm.no_attributes) upd_specs)
       ||>> ((PureThy.add_defs_i false o map Thm.no_attributes)
              [make_spec, fields_spec, extend_spec, truncate_spec])
-      |-> (fn defs as ((sel_defs, upd_defs), derived_defs) => 
+      |-> (fn defs as ((sel_defs, upd_defs), derived_defs) =>
           fold Code.add_default_func sel_defs
           #> fold Code.add_default_func upd_defs
           #> fold Code.add_default_func derived_defs
@@ -2276,12 +2276,10 @@
   P.type_args -- P.name --
     (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const);
 
-val recordP =  
+val _ =
   OuterSyntax.command "record" "define extensible record" K.thy_decl
     (record_decl >> (fn (x, (y, z)) => Toplevel.theory (add_record x y z)));
 
-val _ = OuterSyntax.add_parsers [recordP];
-
 end;
 
 end;
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/HOL/Tools/refute_isar.ML
--- a/src/HOL/Tools/refute_isar.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Tools/refute_isar.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -7,7 +7,7 @@
 syntax.
 *)
 
-structure RefuteIsar =
+structure RefuteIsar: sig end =
 struct
 
 (* ------------------------------------------------------------------------- *)
@@ -56,7 +56,7 @@
 
 	fun refute_parser tokens = (refute_scan_args tokens) |>> refute_trans;
 
-	val refute_cmd = OuterSyntax.improper_command "refute"
+	val _ = OuterSyntax.improper_command "refute"
 		"try to find a model that refutes a given subgoal"
 		OuterKeyword.diag refute_parser;
 
@@ -101,15 +101,9 @@
 	fun refute_params_parser tokens =
 		(refute_params_scan_args tokens) |>> refute_params_trans;
 
-	val refute_params_cmd = OuterSyntax.command "refute_params"
+	val _ = OuterSyntax.command "refute_params"
 		"show/store default parameters for the 'refute' command"
 		OuterKeyword.thy_decl refute_params_parser;
 
 end;
 
-(* ------------------------------------------------------------------------- *)
-(* add the two new commands 'refute' and 'refute_params' to Isabelle/Isar's  *)
-(* outer syntax                                                              *)
-(* ------------------------------------------------------------------------- *)
-
-OuterSyntax.add_parsers [RefuteIsar.refute_cmd, RefuteIsar.refute_params_cmd];
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Tools/res_atp.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -969,8 +969,8 @@
           isar_atp_writeonly (ctxt, chain_ths, goal))
   end;
 
-val _ = OuterSyntax.add_parsers
-  [OuterSyntax.command "sledgehammer" "call automatic theorem provers" OuterKeyword.diag
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep sledgehammer))];
+val _ =
+  OuterSyntax.command "sledgehammer" "call automatic theorem provers" OuterKeyword.diag
+    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep sledgehammer));
 
 end;
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/HOL/Tools/specification_package.ML
--- a/src/HOL/Tools/specification_package.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Tools/specification_package.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -244,7 +244,7 @@
   P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
           Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop)
 
-val specificationP =
+val _ =
   OuterSyntax.command "specification" "define constants by specification" K.thy_goal
     (specification_decl >> (fn (cos,alt_props) =>
                                Toplevel.print o (Toplevel.theory_to_proof
@@ -255,14 +255,12 @@
     (P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
            Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop))
 
-val ax_specificationP =
+val _ =
   OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal
     (ax_specification_decl >> (fn (axname,(cos,alt_props)) =>
                                Toplevel.print o (Toplevel.theory_to_proof
                                                      (process_spec (SOME axname) cos alt_props))))
 
-val _ = OuterSyntax.add_parsers [specificationP,ax_specificationP]
-
 end
 
 
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -273,7 +273,9 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
-val typedeclP =
+val _ = OuterSyntax.keywords ["morphisms"];
+
+val _ =
   OuterSyntax.command "typedecl" "type declaration (HOL)" K.thy_decl
     (P.type_args -- P.name -- P.opt_infix >> (fn ((vs, t), mx) =>
       Toplevel.theory (add_typedecls [(t, vs, mx)])));
@@ -289,14 +291,10 @@
 fun mk_typedef ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
   typedef ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
 
-val typedefP =
+val _ =
   OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" K.thy_goal
     (typedef_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef)));
 
-
-val _ = OuterSyntax.add_keywords ["morphisms"];
-val _ = OuterSyntax.add_parsers [typedeclP, typedefP];
-
 end;
 
 end;
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/HOLCF/IOA/meta_theory/ioa_package.ML
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -481,10 +481,15 @@
   add_rename aut source_aut rename_f;
 
 
-(* parsers *)
+(* outer syntax *)
 
 local structure P = OuterParse and K = OuterKeyword in
 
+val _ = OuterSyntax.keywords ["signature", "actions", "inputs",
+  "outputs", "internals", "states", "initially", "transitions", "pre",
+  "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
+  "rename"];
+
 val actionlist = P.list1 P.term;
 val inputslist = P.$$$ "inputs" |-- P.!!! actionlist;
 val outputslist = P.$$$ "outputs" |-- P.!!! actionlist;
@@ -520,21 +525,10 @@
   (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- (P.!!! (P.name -- (P.$$$ "to" |-- P.term))))))
     >> mk_rename_decl;
 
-val automatonP =
+val _ =
   OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" K.thy_decl
     (ioa_decl >> Toplevel.theory);
 
 end;
 
-
-(* setup outer syntax *)
-
-val _ = OuterSyntax.add_keywords ["signature", "actions", "inputs",
-  "outputs", "internals", "states", "initially", "transitions", "pre",
-  "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
-  "rename"];
-
-val _ = OuterSyntax.add_parsers [automatonP];
-
-
 end;
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/HOLCF/Tools/cont_consts.ML
--- a/src/HOLCF/Tools/cont_consts.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOLCF/Tools/cont_consts.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -99,12 +99,10 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
-val constsP =
+val _ =
   OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl
     (Scan.repeat1 P.const >> (Toplevel.theory o add_consts));
 
-val _ = OuterSyntax.add_parsers [constsP];
-
 end;
 
 end;
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/HOLCF/Tools/domain/domain_extender.ML
--- a/src/HOLCF/Tools/domain/domain_extender.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOLCF/Tools/domain/domain_extender.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -146,6 +146,8 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
+val _ = OuterSyntax.keywords ["lazy"];
+
 val dest_decl =
   P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
     (P.name >> SOME) -- (P.$$$ "::" |-- P.typ)  --| P.$$$ ")" >> P.triple1
@@ -170,14 +172,10 @@
   >> (fn (opt_name, doms) =>
       (case opt_name of NONE => space_implode "_" (map (#1 o #1) doms) | SOME s => s, doms));
 
-val domainP =
+val _ =
   OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl
     (domains_decl >> (Toplevel.theory o add_domain));
 
-
-val _ = OuterSyntax.add_keywords ["lazy"];
-val _ = OuterSyntax.add_parsers [domainP];
-
-end; (* local structure *)
+end;
 
 end;
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/HOLCF/Tools/fixrec_package.ML
--- a/src/HOLCF/Tools/fixrec_package.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOLCF/Tools/fixrec_package.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -299,19 +299,17 @@
 
 (* this builds a parser for a new keyword, fixrec, whose functionality 
 is defined by add_fixrec *)
-val fixrecP =
+val _ =
   OuterSyntax.command "fixrec" "define recursive functions (HOLCF)" K.thy_decl
     (fixrec_decl >> (Toplevel.theory o uncurry add_fixrec));
 
 (* fixpat parser *)
 val fixpat_decl = SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop;
 
-val fixpatP =
+val _ =
   OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl
     (fixpat_decl >> (Toplevel.theory o add_fixpat));
 
-val _ = OuterSyntax.add_parsers [fixrecP, fixpatP];
+end;
 
-end; (* local structure *)
-
-end; (* struct *)
+end;
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/HOLCF/Tools/pcpodef_package.ML
--- a/src/HOLCF/Tools/pcpodef_package.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOLCF/Tools/pcpodef_package.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -184,7 +184,7 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
-(* copied from HOL/Tools/typedef_package.ML *)
+(* cf. HOL/Tools/typedef_package.ML *)
 val typedef_proof_decl =
   Scan.optional (P.$$$ "(" |--
       ((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s)))
@@ -196,18 +196,16 @@
   (if pcpo then pcpodef_proof else cpodef_proof)
     ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
 
-val pcpodefP =
+val _ =
   OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
     (typedef_proof_decl >>
       (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)));
 
-val cpodefP =
+val _ =
   OuterSyntax.command "cpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
     (typedef_proof_decl >>
       (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)));
 
-val _ = OuterSyntax.add_parsers [pcpodefP, cpodefP];
-
 end;
 
 end;
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/Provers/classical.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -1084,7 +1084,7 @@
 
 (** outer syntax **)
 
-val print_clasetP =
+val _ =
   OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner"
     OuterKeyword.diag
     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep
@@ -1092,7 +1092,4 @@
         (Context.cases print_claset print_local_claset)
         (print_local_claset o Proof.context_of)))));
 
-val _ = OuterSyntax.add_parsers [print_clasetP];
-
-
 end;
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/Pure/Proof/extraction.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -759,7 +759,7 @@
 
 val parse_vars = Scan.optional (P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") [];
 
-val realizersP =
+val _ =
   OuterSyntax.command "realizers"
   "specify realizers for primitive axioms / theorems, together with correctness proof"
   K.thy_decl
@@ -768,23 +768,21 @@
        (map (fn (((a, vs), s1), s2) =>
          (PureThy.get_thm thy (Name a), (vs, s1, s2))) xs) thy)));
 
-val realizabilityP =
+val _ =
   OuterSyntax.command "realizability"
   "add equations characterizing realizability" K.thy_decl
   (Scan.repeat1 P.string >> (Toplevel.theory o add_realizes_eqns));
 
-val typeofP =
+val _ =
   OuterSyntax.command "extract_type"
   "add equations characterizing type of extracted program" K.thy_decl
   (Scan.repeat1 P.string >> (Toplevel.theory o add_typeof_eqns));
 
-val extractP =
+val _ =
   OuterSyntax.command "extract" "extract terms from proofs" K.thy_decl
     (Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory
       (fn thy => extract (map (apfst (PureThy.get_thm thy o Name)) xs) thy)));
 
-val _ = OuterSyntax.add_parsers [realizersP, realizabilityP, typeofP, extractP];
-
 val etype_of = etype_of o add_syntax;
 
 end;
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -231,36 +231,36 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
-val undoP = (*undo without output*)
+fun undoP () = (*undo without output*)
   OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
     (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
 
-val restartP =
+fun restartP () =
   OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
     (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
 
-val kill_proofP =
+fun kill_proofP () =
   OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
     (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
 
-val inform_file_processedP =
+fun inform_file_processedP () =
   OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
     (P.name >> (fn file => Toplevel.no_timing o
       Toplevel.init_empty (vacuous_inform_file_processed file) o
       Toplevel.kill o
       Toplevel.init_empty (proper_inform_file_processed file)));
 
-val inform_file_retractedP =
+fun inform_file_retractedP () =
   OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
     (P.name >> (Toplevel.no_timing oo
       (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
 
-val process_pgipP =
+fun process_pgipP () =
   OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
     (P.text >> (Toplevel.no_timing oo
       (fn txt => Toplevel.imperative (fn () => ProofGeneralPgip.process_pgip txt))));
 
-fun init_outer_syntax () = OuterSyntax.add_parsers
+fun init_outer_syntax () = List.app (fn f => f ())
  [undoP, restartP, kill_proofP, inform_file_processedP, inform_file_retractedP, process_pgipP];
 
 end;
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -1125,21 +1125,13 @@
 end
 
 
-local
 (* Extra command for embedding prover-control inside document (obscure/debug usage). *)
 
-val process_pgipP =
+fun init_outer_syntax () =
   OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" OuterKeyword.control
     (OuterParse.text >> (Toplevel.no_timing oo
       (fn txt => Toplevel.imperative (fn () => process_pgip_plain txt))));
 
-in
-
- fun init_outer_syntax () = OuterSyntax.add_parsers [process_pgipP];
-
-end
-
-
 
 (* init *)
 
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/Pure/Tools/invoke.ML
--- a/src/Pure/Tools/invoke.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/Pure/Tools/invoke.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -115,7 +115,7 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
-val invokeP =
+val _ =
   OuterSyntax.command "invoke"
     "schematic invocation of locale expression in proof context"
     (K.tag_proof K.prf_goal)
@@ -123,8 +123,6 @@
       >> (fn (((name, expr), (insts, _)), fixes) =>
           Toplevel.print o Toplevel.proof' (invoke name expr insts fixes)));
 
-val _ = OuterSyntax.add_parsers [invokeP];
-
 end;
 
 end;
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/Pure/Tools/named_thms.ML
--- a/src/Pure/Tools/named_thms.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/Pure/Tools/named_thms.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -36,10 +36,10 @@
 val setup =
   Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)];
 
-val _ = OuterSyntax.add_parsers
- [OuterSyntax.improper_command ("print_" ^ name ^ "_rules") ("print " ^ description)
+val _ =
+  OuterSyntax.improper_command ("print_" ^ name ^ "_rules") ("print " ^ description)
     OuterKeyword.diag
     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
-      Toplevel.keep (Pretty.writeln o pretty o Toplevel.context_of)))];
+      Toplevel.keep (Pretty.writeln o pretty o Toplevel.context_of)));
 
 end;
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/Pure/codegen.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -1100,6 +1100,8 @@
 
 structure P = OuterParse and K = OuterKeyword;
 
+val _ = OuterSyntax.keywords ["attach", "file", "contains"];
+
 fun strip_whitespace s = implode (fst (take_suffix (equal "\n" orf equal " ")
   (snd (take_prefix (equal "\n" orf equal " ") (explode s))))) ^ "\n";
 
@@ -1107,7 +1109,7 @@
   Scan.optional (P.$$$ "(" |-- P.xname --| P.$$$ ")") "" --
     (P.verbatim >> strip_whitespace));
 
-val assoc_typeP =
+val _ =
   OuterSyntax.command "types_code"
   "associate types with target language types" K.thy_decl
     (Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
@@ -1115,7 +1117,7 @@
        (fn ((name, mfx), aux) => (name, (parse_mixfix
          (Syntax.read_typ_global thy) mfx, aux)))) xs thy)));
 
-val assoc_constP =
+val _ =
   OuterSyntax.command "consts_code"
   "associate constants with target language code" K.thy_decl
     (Scan.repeat1
@@ -1152,12 +1154,12 @@
            else map_modules (Symtab.update (module, gr)) thy)
      end));
 
-val code_libraryP =
+val _ =
   OuterSyntax.command "code_library"
     "generates code for terms (one structure for each theory)" K.thy_decl
     (parse_code true);
 
-val code_moduleP =
+val _ =
   OuterSyntax.command "code_module"
     "generates code for terms (single structure, incremental)" K.thy_decl
     (parse_code false);
@@ -1174,13 +1176,13 @@
   (P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn thy =>
     fn (x, ys) => (x, (v, Syntax.read_typ_global thy s) :: ys))) xs;
 
-val test_paramsP =
+val _ =
   OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl
     (P.$$$ "[" |-- P.list1 parse_test_params --| P.$$$ "]" >>
       (fn fs => Toplevel.theory (fn thy =>
          map_test_params (Library.apply (map (fn f => f thy) fs)) thy)));
 
-val testP =
+val _ =
   OuterSyntax.command "quickcheck" "try to find counterexample for subgoal" K.diag
   (Scan.option (P.$$$ "[" |-- P.list1
     (   parse_test_params >> (fn f => fn thy => apfst (f thy))
@@ -1191,15 +1193,10 @@
         (get_test_params (Toplevel.theory_of st), [])) g [] |>
       pretty_counterex (Toplevel.context_of st) |> Pretty.writeln)));
 
-val valueP =
+val _ =
   OuterSyntax.improper_command "value" "read, evaluate and print term" K.diag
     (P.term >> (Toplevel.no_timing oo print_evaluated_term));
 
-val _ = OuterSyntax.add_keywords ["attach", "file", "contains"];
-
-val _ = OuterSyntax.add_parsers
-  [assoc_typeP, assoc_constP, code_libraryP, code_moduleP, test_paramsP, testP, valueP];
-
 end;
 
 val auto_quickcheck = Codegen.auto_quickcheck;
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/Tools/code/code_package.ML
--- a/src/Tools/code/code_package.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/Tools/code/code_package.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -558,14 +558,14 @@
      -- Scan.optional (P.$$$ "(" |-- P.arguments --| P.$$$ ")") []
   ) >> (fn (raw_cs, seris) => cmd raw_cs seris));
 
-val _ = OuterSyntax.add_keywords [inK, module_nameK, fileK];
+val _ = OuterSyntax.keywords [inK, module_nameK, fileK];
 
 val (codeK, code_thmsK, code_depsK, code_propsK) =
   ("export_code", "code_thms", "code_deps", "code_props");
 
 in
 
-val codeP =
+val _ =
   OuterSyntax.improper_command codeK "generate executable code for constants"
     K.diag (P.!!! (code_exprP code_cmd) >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
 
@@ -574,24 +574,22 @@
    of SOME f => (writeln "Now generating code..."; f thy)
     | NONE => error ("Bad directive " ^ quote cmd);
 
-val code_thmsP =
+val _ =
   OuterSyntax.improper_command code_thmsK "print system of defining equations for code" OuterKeyword.diag
     (Scan.repeat P.term
       >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
         o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
 
-val code_depsP =
+val _ =
   OuterSyntax.improper_command code_depsK "visualize dependencies of defining equations for code" OuterKeyword.diag
     (Scan.repeat P.term
       >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
         o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
 
-val code_propsP =
+val _ =
   OuterSyntax.command code_propsK "generate characteristic properties for executable constants"
     K.thy_decl (P.!!! (code_exprP code_props_cmd) >> Toplevel.theory);
 
-val _ = OuterSyntax.add_parsers [codeP, code_thmsP, code_depsP, code_propsP];
-
 end; (*local*)
 
 end; (*struct*)
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/Tools/code/code_target.ML
--- a/src/Tools/code/code_target.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/Tools/code/code_target.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -2091,7 +2091,10 @@
 
 val add_haskell_monad = gen_add_haskell_monad CodeUnit.read_const;
 
-val code_classP =
+
+val _ = OuterSyntax.keywords [infixK, infixlK, infixrK];
+
+val _ =
   OuterSyntax.command code_classK "define code syntax for class" K.thy_decl (
     parse_multi_syntax P.xname
       (Scan.option (P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
@@ -2100,7 +2103,7 @@
           fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)
   );
 
-val code_instanceP =
+val _ =
   OuterSyntax.command code_instanceK "define code syntax for instance" K.thy_decl (
     parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname)
       ((P.minus >> K true) || Scan.succeed false)
@@ -2108,55 +2111,50 @@
           fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns)
   );
 
-val code_typeP =
+val _ =
   OuterSyntax.command code_typeK "define code syntax for type constructor" K.thy_decl (
     parse_multi_syntax P.xname (parse_syntax I)
     >> (Toplevel.theory oo fold) (fn (target, syns) =>
           fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns)
   );
 
-val code_constP =
+val _ =
   OuterSyntax.command code_constK "define code syntax for constant" K.thy_decl (
     parse_multi_syntax P.term (parse_syntax fst)
     >> (Toplevel.theory oo fold) (fn (target, syns) =>
           fold (fn (raw_const, syn) => add_syntax_const_cmd target raw_const (no_bindings syn)) syns)
   );
 
-val code_monadP =
+val _ =
   OuterSyntax.command code_monadK "define code syntax for Haskell monads" K.thy_decl (
     P.term -- P.term -- P.term
     >> (fn ((raw_run, raw_mbind), raw_kbind) => Toplevel.theory 
           (add_haskell_monad raw_run raw_mbind raw_kbind))
   );
 
-val code_reservedP =
+val _ =
   OuterSyntax.command code_reservedK "declare words as reserved for target language" K.thy_decl (
     P.name -- Scan.repeat1 P.name
     >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds)
   );
 
-val code_modulenameP =
+val _ =
   OuterSyntax.command code_modulenameK "alias module to other name" K.thy_decl (
     P.name -- Scan.repeat1 (P.name -- P.name)
     >> (fn (target, modlnames) => (Toplevel.theory o fold (add_modl_alias target)) modlnames)
   );
 
-val code_moduleprologP =
+val _ =
   OuterSyntax.command code_moduleprologK "add prolog to module" K.thy_decl (
     P.name -- Scan.repeat1 (P.name -- (P.text >> (fn "-" => NONE | s => SOME s)))
     >> (fn (target, prologs) => (Toplevel.theory o fold (add_modl_prolog target)) prologs)
   );
 
-val code_exceptionP =
+val _ =
   OuterSyntax.command code_exceptionK "permit exceptions for constant" K.thy_decl (
     Scan.repeat1 P.term >> (Toplevel.theory o fold allow_exception_cmd)
   );
 
-val _ = OuterSyntax.add_keywords [infixK, infixlK, infixrK];
-
-val _ = OuterSyntax.add_parsers [code_classP, code_instanceP, code_typeP, code_constP,
-  code_reservedP, code_modulenameP, code_moduleprologP, code_monadP, code_exceptionP];
-
 
 (*including serializer defaults*)
 val setup =
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/Tools/induct.ML
--- a/src/Tools/induct.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/Tools/induct.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -161,10 +161,10 @@
     |> Pretty.chunks |> Pretty.writeln
   end;
 
-val _ = OuterSyntax.add_parsers [
+val _ =
   OuterSyntax.improper_command "print_induct_rules" "print induction and cases rules"
     OuterKeyword.diag (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
-      Toplevel.keep (print_rules o Toplevel.context_of)))];
+      Toplevel.keep (print_rules o Toplevel.context_of)));
 
 
 (* access rules *)
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/Tools/nbe.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -410,12 +410,10 @@
 
 val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
 
-val nbeP =
+val _ =
   OuterSyntax.improper_command "normal_form" "normalize term by evaluation" K.diag
     (opt_modes -- P.typ >> (Toplevel.keep o norm_print_term_cmd));
 
-val _ = OuterSyntax.add_parsers [nbeP];
-
 end;
 
 end;
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -422,11 +422,9 @@
 
 val coind_prefix = if coind then "co" else "";
 
-val inductiveP = OuterSyntax.command (coind_prefix ^ "datatype")
+val _ = OuterSyntax.command (coind_prefix ^ "datatype")
   ("define " ^ coind_prefix ^ "datatype") K.thy_decl datatype_decl;
 
-val _ = OuterSyntax.add_parsers [inductiveP];
-
 end;
 
 end;
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/ZF/Tools/ind_cases.ML
--- a/src/ZF/Tools/ind_cases.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/ZF/Tools/ind_cases.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -76,15 +76,11 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
-val ind_cases =
-  P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop)
-  >> (Toplevel.theory o inductive_cases);
-
-val inductive_casesP =
+val _ =
   OuterSyntax.command "inductive_cases"
-    "create simplified instances of elimination rules (improper)" K.thy_script ind_cases;
-
-val _ = OuterSyntax.add_parsers [inductive_casesP];
+    "create simplified instances of elimination rules (improper)" K.thy_script
+    (P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop)
+      >> (Toplevel.theory o inductive_cases));
 
 end;
 
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -188,6 +188,8 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
+val _ = OuterSyntax.keywords ["elimination", "induction", "case_eqns", "recursor_eqns"];
+
 val rep_datatype_decl =
   (P.$$$ "elimination" |-- P.!!! SpecParse.xthm) --
   (P.$$$ "induction" |-- P.!!! SpecParse.xthm) --
@@ -195,13 +197,10 @@
   Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! SpecParse.xthms1) []
   >> (fn (((x, y), z), w) => rep_datatype x y z w);
 
-val rep_datatypeP =
+val _ =
   OuterSyntax.command "rep_datatype" "represent existing set inductively" K.thy_decl
     (rep_datatype_decl >> Toplevel.theory);
 
-val _ = OuterSyntax.add_keywords ["elimination", "induction", "case_eqns", "recursor_eqns"];
-val _ = OuterSyntax.add_parsers [rep_datatypeP];
-
 end;
 
 end;
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -576,6 +576,9 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
+val _ = OuterSyntax.keywords
+  ["domains", "intros", "monos", "con_defs", "type_intros", "type_elims"];
+
 fun mk_ind (((((doms, intrs), monos), con_defs), type_intrs), type_elims) =
   #1 o add_inductive doms (map P.triple_swap intrs) (monos, con_defs, type_intrs, type_elims);
 
@@ -590,13 +593,9 @@
   Scan.optional (P.$$$ "type_elims" |-- P.!!! SpecParse.xthms1) []
   >> (Toplevel.theory o mk_ind);
 
-val inductiveP = OuterSyntax.command (co_prefix ^ "inductive")
+val _ = OuterSyntax.command (co_prefix ^ "inductive")
   ("define " ^ co_prefix ^ "inductive sets") K.thy_decl ind_decl;
 
-val _ = OuterSyntax.add_keywords
-  ["domains", "intros", "monos", "con_defs", "type_intros", "type_elims"];
-val _ = OuterSyntax.add_parsers [inductiveP];
-
 end;
 
 end;
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/ZF/Tools/primrec_package.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -203,18 +203,12 @@
 
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterKeyword in
-
-val primrec_decl = Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
+structure P = OuterParse and K = OuterKeyword;
 
-val primrecP =
+val _ =
   OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
-    (primrec_decl >> (Toplevel.theory o (#1 oo (add_primrec o map P.triple_swap))));
-
-val _ = OuterSyntax.add_parsers [primrecP];
+    (Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop)
+      >> (Toplevel.theory o (#1 oo (add_primrec o map P.triple_swap))));
 
 end;
 
-end;
-
-
diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/ZF/Tools/typechk.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -118,10 +118,10 @@
      Args.del -- Args.colon >> K (I, TC_del)]
   (fn ctxt => Method.SIMPLE_METHOD (CHANGED (typecheck_tac ctxt)));
 
-val _ = OuterSyntax.add_parsers
-  [OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag
+val _ =
+  OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag
     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
-      Toplevel.keep (print_tcset o Toplevel.context_of)))];
+      Toplevel.keep (print_tcset o Toplevel.context_of)));
 
 
 (* theory setup *)