simplified interfaces for outer syntax;
authorwenzelm
Sat Oct 06 16:50:04 2007 +0200 (2007-10-06)
changeset 24867e5b55d7be9bb
parent 24866 6e6d9e80ebb4
child 24868 2990c327d8c6
simplified interfaces for outer syntax;
NEWS
src/HOL/Import/import_syntax.ML
src/HOL/Library/Eval.thy
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_package.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Orderings.thy
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/function_package/fundef_datatype.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/inductive_set_package.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/recdef_package.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/refute_isar.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/specification_package.ML
src/HOL/Tools/typedef_package.ML
src/HOLCF/IOA/meta_theory/ioa_package.ML
src/HOLCF/Tools/cont_consts.ML
src/HOLCF/Tools/domain/domain_extender.ML
src/HOLCF/Tools/fixrec_package.ML
src/HOLCF/Tools/pcpodef_package.ML
src/Provers/classical.ML
src/Pure/Proof/extraction.ML
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/Tools/invoke.ML
src/Pure/Tools/named_thms.ML
src/Pure/codegen.ML
src/Tools/code/code_package.ML
src/Tools/code/code_target.ML
src/Tools/induct.ML
src/Tools/nbe.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/NEWS	Sat Oct 06 16:41:22 2007 +0200
     1.2 +++ b/NEWS	Sat Oct 06 16:50:04 2007 +0200
     1.3 @@ -1337,6 +1337,11 @@
     1.4  quasi-functional intermediate checkpoint, both in interactive and
     1.5  batch mode.
     1.6  
     1.7 +* Isar: simplified interfaces for outer syntax.  Renamed
     1.8 +OuterSyntax.add_keywords to OuterSyntax.keywords.  Removed
     1.9 +OuterSyntax.add_parsers -- this functionality is now included in
    1.10 +OuterSyntax.command etc.  INCOMPATIBILITY.
    1.11 +
    1.12  * Simplifier: the simpset of a running simplification process now
    1.13  contains a proof context (cf. Simplifier.the_context), which is the
    1.14  very context that the initial simpset has been retrieved from (by
     2.1 --- a/src/HOL/Import/import_syntax.ML	Sat Oct 06 16:41:22 2007 +0200
     2.2 +++ b/src/HOL/Import/import_syntax.ML	Sat Oct 06 16:50:04 2007 +0200
     2.3 @@ -5,7 +5,7 @@
     2.4  
     2.5  signature HOL4_IMPORT_SYNTAX =
     2.6  sig
     2.7 -    type token = OuterSyntax.token
     2.8 +    type token = OuterLex.token
     2.9      type command  = token list -> (theory -> theory) * token list 
    2.10  
    2.11      val import_segment: token list -> (theory -> theory) * token list
    2.12 @@ -32,7 +32,7 @@
    2.13  structure HOL4ImportSyntax :> HOL4_IMPORT_SYNTAX =
    2.14  struct
    2.15  
    2.16 -type token = OuterSyntax.token
    2.17 +type token = OuterLex.token
    2.18  type command  = token list -> (theory -> theory) * token list 
    2.19  
    2.20  local structure P = OuterParse and K = OuterKeyword in
    2.21 @@ -222,61 +222,59 @@
    2.22  fun fl_dump toks  = Scan.succeed flush_dump toks
    2.23  val append_dump = (P.verbatim || P.string) >> add_dump
    2.24  
    2.25 -val parsers = 
    2.26 -  [OuterSyntax.command "import_segment"
    2.27 +fun setup () =
    2.28 +  (OuterSyntax.keywords[">"];
    2.29 +   OuterSyntax.command "import_segment"
    2.30  		       "Set import segment name"
    2.31 -		       K.thy_decl (import_segment >> Toplevel.theory),
    2.32 +		       K.thy_decl (import_segment >> Toplevel.theory);
    2.33     OuterSyntax.command "import_theory"
    2.34  		       "Set default HOL4 theory name"
    2.35 -		       K.thy_decl (import_theory >> Toplevel.theory),
    2.36 +		       K.thy_decl (import_theory >> Toplevel.theory);
    2.37     OuterSyntax.command "end_import"
    2.38  		       "End HOL4 import"
    2.39 -		       K.thy_decl (end_import >> Toplevel.theory),
    2.40 +		       K.thy_decl (end_import >> Toplevel.theory);
    2.41     OuterSyntax.command "skip_import_dir" 
    2.42                         "Sets caching directory for skipping importing"
    2.43 -                       K.thy_decl (skip_import_dir >> Toplevel.theory),
    2.44 +                       K.thy_decl (skip_import_dir >> Toplevel.theory);
    2.45     OuterSyntax.command "skip_import" 
    2.46                         "Switches skipping importing on or off"
    2.47 -                       K.thy_decl (skip_import >> Toplevel.theory),		      
    2.48 +                       K.thy_decl (skip_import >> Toplevel.theory);		      
    2.49     OuterSyntax.command "setup_theory"
    2.50  		       "Setup HOL4 theory replaying"
    2.51 -		       K.thy_decl (setup_theory >> Toplevel.theory),
    2.52 +		       K.thy_decl (setup_theory >> Toplevel.theory);
    2.53     OuterSyntax.command "end_setup"
    2.54  		       "End HOL4 setup"
    2.55 -		       K.thy_decl (end_setup >> Toplevel.theory),
    2.56 +		       K.thy_decl (end_setup >> Toplevel.theory);
    2.57     OuterSyntax.command "setup_dump"
    2.58  		       "Setup the dump file name"
    2.59 -		       K.thy_decl (set_dump >> Toplevel.theory),
    2.60 +		       K.thy_decl (set_dump >> Toplevel.theory);
    2.61     OuterSyntax.command "append_dump"
    2.62  		       "Add text to dump file"
    2.63 -		       K.thy_decl (append_dump >> Toplevel.theory),
    2.64 +		       K.thy_decl (append_dump >> Toplevel.theory);
    2.65     OuterSyntax.command "flush_dump"
    2.66  		       "Write the dump to file"
    2.67 -		       K.thy_decl (fl_dump >> Toplevel.theory),
    2.68 +		       K.thy_decl (fl_dump >> Toplevel.theory);
    2.69     OuterSyntax.command "ignore_thms"
    2.70  		       "Theorems to ignore in next HOL4 theory import"
    2.71 -		       K.thy_decl (ignore_thms >> Toplevel.theory),
    2.72 +		       K.thy_decl (ignore_thms >> Toplevel.theory);
    2.73     OuterSyntax.command "type_maps"
    2.74  		       "Map HOL4 type names to existing Isabelle/HOL type names"
    2.75 -		       K.thy_decl (type_maps >> Toplevel.theory),
    2.76 +		       K.thy_decl (type_maps >> Toplevel.theory);
    2.77     OuterSyntax.command "def_maps"
    2.78  		       "Map HOL4 constant names to their primitive definitions"
    2.79 -		       K.thy_decl (def_maps >> Toplevel.theory),
    2.80 +		       K.thy_decl (def_maps >> Toplevel.theory);
    2.81     OuterSyntax.command "thm_maps"
    2.82  		       "Map HOL4 theorem names to existing Isabelle/HOL theorem names"
    2.83 -		       K.thy_decl (thm_maps >> Toplevel.theory),
    2.84 +		       K.thy_decl (thm_maps >> Toplevel.theory);
    2.85     OuterSyntax.command "const_renames"
    2.86  		       "Rename HOL4 const names"
    2.87 -		       K.thy_decl (const_renames >> Toplevel.theory),
    2.88 +		       K.thy_decl (const_renames >> Toplevel.theory);
    2.89     OuterSyntax.command "const_moves"
    2.90  		       "Rename HOL4 const names to other HOL4 constants"
    2.91 -		       K.thy_decl (const_moves >> Toplevel.theory),
    2.92 +		       K.thy_decl (const_moves >> Toplevel.theory);
    2.93     OuterSyntax.command "const_maps"
    2.94  		       "Map HOL4 const names to existing Isabelle/HOL const names"
    2.95 -		       K.thy_decl (const_maps >> Toplevel.theory)]
    2.96 -
    2.97 -fun setup () = (OuterSyntax.add_keywords[">"];
    2.98 -		OuterSyntax.add_parsers parsers)
    2.99 +		       K.thy_decl (const_maps >> Toplevel.theory));
   2.100  
   2.101  end
   2.102  
     3.1 --- a/src/HOL/Library/Eval.thy	Sat Oct 06 16:41:22 2007 +0200
     3.2 +++ b/src/HOL/Library/Eval.thy	Sat Oct 06 16:50:04 2007 +0200
     3.3 @@ -213,14 +213,11 @@
     3.4  *}
     3.5  
     3.6  ML {*
     3.7 -val valueP =
     3.8    OuterSyntax.improper_command "value" "read, evaluate and print term" OuterKeyword.diag
     3.9      (Scan.option (OuterParse.$$$ "(" |-- OuterParse.name --| OuterParse.$$$ ")")
    3.10      -- OuterParse.term
    3.11        >> (fn (some_name, t) => Toplevel.no_timing o Toplevel.keep
    3.12             (Eval.evaluate_cmd some_name t)));
    3.13 -
    3.14 -val _ = OuterSyntax.add_parsers [valueP];
    3.15  *}
    3.16  
    3.17  end
     4.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sat Oct 06 16:41:22 2007 +0200
     4.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Oct 06 16:50:04 2007 +0200
     4.3 @@ -947,10 +947,8 @@
     4.4  (* syntax und parsing *)
     4.5  structure P = OuterParse and K = OuterKeyword;
     4.6  
     4.7 -val atom_declP =
     4.8 +val _ =
     4.9    OuterSyntax.command "atom_decl" "Declare new kinds of atoms" K.thy_decl
    4.10      (Scan.repeat1 P.name >> (Toplevel.theory o create_nom_typedecls));
    4.11  
    4.12 -val _ = OuterSyntax.add_parsers [atom_declP];
    4.13 -
    4.14  end;
     5.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Sat Oct 06 16:41:22 2007 +0200
     5.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Sat Oct 06 16:50:04 2007 +0200
     5.3 @@ -511,22 +511,21 @@
     5.4  
     5.5  local structure P = OuterParse and K = OuterKeyword in
     5.6  
     5.7 -val nominal_inductiveP =
     5.8 +val _ = OuterSyntax.keywords ["avoids"];
     5.9 +
    5.10 +val _ =
    5.11    OuterSyntax.command "nominal_inductive"
    5.12      "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal
    5.13      (P.name -- Scan.optional (P.$$$ "avoids" |-- P.and_list1 (P.name --
    5.14        (P.$$$ ":" |-- Scan.repeat1 P.name))) [] >> (fn (name, avoids) =>
    5.15          Toplevel.print o Toplevel.theory_to_proof (prove_strong_ind name avoids)));
    5.16  
    5.17 -val equivarianceP =
    5.18 +val _ =
    5.19    OuterSyntax.command "equivariance"
    5.20      "prove equivariance for inductive predicate involving nominal datatypes" K.thy_decl
    5.21      (P.name -- Scan.optional (P.$$$ "[" |-- P.list1 P.name --| P.$$$ "]") [] >>
    5.22        (fn (name, atoms) => Toplevel.theory (prove_eqvt name atoms)));
    5.23  
    5.24 -val _ = OuterSyntax.add_keywords ["avoids"];
    5.25 -val _ = OuterSyntax.add_parsers [nominal_inductiveP, equivarianceP];
    5.26 -
    5.27  end;
    5.28  
    5.29  end
     6.1 --- a/src/HOL/Nominal/nominal_package.ML	Sat Oct 06 16:41:22 2007 +0200
     6.2 +++ b/src/HOL/Nominal/nominal_package.ML	Sat Oct 06 16:50:04 2007 +0200
     6.3 @@ -2094,12 +2094,10 @@
     6.4        (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
     6.5    in add_nominal_datatype false names specs end;
     6.6  
     6.7 -val nominal_datatypeP =
     6.8 +val _ =
     6.9    OuterSyntax.command "nominal_datatype" "define inductive datatypes" K.thy_decl
    6.10      (P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
    6.11  
    6.12 -val _ = OuterSyntax.add_parsers [nominal_datatypeP];
    6.13 -
    6.14  end;
    6.15  
    6.16  end
     7.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Sat Oct 06 16:41:22 2007 +0200
     7.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Sat Oct 06 16:50:04 2007 +0200
     7.3 @@ -416,6 +416,8 @@
     7.4  
     7.5  local structure P = OuterParse and K = OuterKeyword in
     7.6  
     7.7 +val _ = OuterSyntax.keywords ["invariant", "freshness_context"];
     7.8 +
     7.9  val parser1 = P.$$$ "freshness_context" |-- P.$$$ ":" |-- (P.term >> SOME);
    7.10  val parser2 =
    7.11    P.$$$ "invariant" |-- P.$$$ ":" |--
    7.12 @@ -434,16 +436,13 @@
    7.13  val primrec_decl =
    7.14    options -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
    7.15  
    7.16 -val primrecP =
    7.17 +val _ =
    7.18    OuterSyntax.command "nominal_primrec" "define primitive recursive functions on nominal datatypes" K.thy_goal
    7.19      (primrec_decl >> (fn ((unchecked, (alt_name, (invs, fctxt))), eqns) =>
    7.20        Toplevel.print o Toplevel.theory_to_proof
    7.21          ((if unchecked then add_primrec_unchecked else add_primrec) alt_name invs fctxt
    7.22            (map P.triple_swap eqns))));
    7.23  
    7.24 -val _ = OuterSyntax.add_parsers [primrecP];
    7.25 -val _ = OuterSyntax.add_keywords ["invariant", "freshness_context"];
    7.26 -
    7.27  end;
    7.28  
    7.29  
     8.1 --- a/src/HOL/Orderings.thy	Sat Oct 06 16:41:22 2007 +0200
     8.2 +++ b/src/HOL/Orderings.thy	Sat Oct 06 16:50:04 2007 +0200
     8.3 @@ -346,7 +346,7 @@
     8.4      (Context.cases (print_structures o ProofContext.init) print_structures)
     8.5      (print_structures o Proof.context_of));
     8.6  
     8.7 -val printP =
     8.8 +val _ =
     8.9    OuterSyntax.improper_command "print_orders"
    8.10      "print order structures available to transitivity reasoner" OuterKeyword.diag
    8.11      (Scan.succeed (Toplevel.no_timing o print));
    8.12 @@ -354,11 +354,10 @@
    8.13  
    8.14  (** Setup **)
    8.15  
    8.16 -val setup = let val _ = OuterSyntax.add_parsers [printP] in
    8.17 -    Method.add_methods [("order", Method.ctxt_args (Method.SIMPLE_METHOD' o order_tac []),
    8.18 -      "normalisation of algebraic structure")] #>
    8.19 -    Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")]
    8.20 -  end;
    8.21 +val setup =
    8.22 +  Method.add_methods
    8.23 +    [("order", Method.ctxt_args (Method.SIMPLE_METHOD' o order_tac []), "transitivity reasoner")] #>
    8.24 +  Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")];
    8.25  
    8.26  end;
    8.27  
     9.1 --- a/src/HOL/Tools/datatype_package.ML	Sat Oct 06 16:41:22 2007 +0200
     9.2 +++ b/src/HOL/Tools/datatype_package.ML	Sat Oct 06 16:50:04 2007 +0200
     9.3 @@ -908,6 +908,8 @@
     9.4  
     9.5  local structure P = OuterParse and K = OuterKeyword in
     9.6  
     9.7 +val _ = OuterSyntax.keywords ["distinct", "inject", "induction"];
     9.8 +
     9.9  val datatype_decl =
    9.10    Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --
    9.11      (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
    9.12 @@ -919,7 +921,7 @@
    9.13        (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
    9.14    in snd o add_datatype false names specs end;
    9.15  
    9.16 -val datatypeP =
    9.17 +val _ =
    9.18    OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl
    9.19      (P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
    9.20  
    9.21 @@ -932,14 +934,10 @@
    9.22  
    9.23  fun mk_rep_datatype (((opt_ts, dss), iss), ind) = #2 o rep_datatype opt_ts dss iss ind;
    9.24  
    9.25 -val rep_datatypeP =
    9.26 +val _ =
    9.27    OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_decl
    9.28      (rep_datatype_decl >> (Toplevel.theory o mk_rep_datatype));
    9.29  
    9.30 -
    9.31 -val _ = OuterSyntax.add_keywords ["distinct", "inject", "induction"];
    9.32 -val _ = OuterSyntax.add_parsers [datatypeP, rep_datatypeP];
    9.33 -
    9.34  end;
    9.35  
    9.36  
    10.1 --- a/src/HOL/Tools/function_package/fundef_datatype.ML	Sat Oct 06 16:41:22 2007 +0200
    10.2 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Sat Oct 06 16:50:04 2007 +0200
    10.3 @@ -302,13 +302,12 @@
    10.4        |> by_pat_completeness_simp
    10.5        |> termination_by_lexicographic_order
    10.6  
    10.7 -val funP =
    10.8 +val _ =
    10.9    OuterSyntax.command "fun" "define general recursive functions (short version)" K.thy_decl
   10.10    (fundef_parser fun_config
   10.11       >> (fn ((config, fixes), (flags, statements)) =>
   10.12              (Toplevel.local_theory (target_of config) (fun_cmd config fixes statements flags))));
   10.13  
   10.14 -val _ = OuterSyntax.add_parsers [funP];
   10.15  end
   10.16  
   10.17  end
    11.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Sat Oct 06 16:41:22 2007 +0200
    11.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Sat Oct 06 16:50:04 2007 +0200
    11.3 @@ -268,24 +268,22 @@
    11.4  
    11.5  local structure P = OuterParse and K = OuterKeyword in
    11.6  
    11.7 -val functionP =
    11.8 +val _ = OuterSyntax.keywords ["sequential", "otherwise"];
    11.9 +
   11.10 +val _ =
   11.11    OuterSyntax.command "function" "define general recursive functions" K.thy_goal
   11.12    (fundef_parser default_config
   11.13       >> (fn ((config, fixes), (flags, statements)) =>
   11.14              Toplevel.local_theory_to_proof (target_of config) (add_fundef fixes statements config flags)
   11.15              #> Toplevel.print));
   11.16  
   11.17 -val terminationP =
   11.18 +val _ =
   11.19    OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
   11.20    (P.opt_target -- Scan.option P.term
   11.21      >> (fn (target, name) =>
   11.22             Toplevel.print o
   11.23             Toplevel.local_theory_to_proof target (setup_termination_proof name)));
   11.24  
   11.25 -val _ = OuterSyntax.add_parsers [functionP];
   11.26 -val _ = OuterSyntax.add_parsers [terminationP];
   11.27 -val _ = OuterSyntax.add_keywords ["sequential", "otherwise"];
   11.28 -
   11.29  end;
   11.30  
   11.31  
    12.1 --- a/src/HOL/Tools/inductive_package.ML	Sat Oct 06 16:41:22 2007 +0200
    12.2 +++ b/src/HOL/Tools/inductive_package.ML	Sat Oct 06 16:50:04 2007 +0200
    12.3 @@ -923,6 +923,8 @@
    12.4  
    12.5  local structure P = OuterParse and K = OuterKeyword in
    12.6  
    12.7 +val _ = OuterSyntax.keywords ["monos"];
    12.8 +
    12.9  (* FIXME tmp *)
   12.10  fun flatten_specification specs = specs |> maps
   12.11    (fn (a, (concl, [])) => concl |> map
   12.12 @@ -945,22 +947,15 @@
   12.13  
   12.14  val ind_decl = gen_ind_decl add_ind_def;
   12.15  
   12.16 -val inductiveP =
   12.17 -  OuterSyntax.command "inductive" "define inductive predicates" K.thy_decl (ind_decl false);
   12.18 +val _ = OuterSyntax.command "inductive" "define inductive predicates" K.thy_decl (ind_decl false);
   12.19 +val _ = OuterSyntax.command "coinductive" "define coinductive predicates" K.thy_decl (ind_decl true);
   12.20  
   12.21 -val coinductiveP =
   12.22 -  OuterSyntax.command "coinductive" "define coinductive predicates" K.thy_decl (ind_decl true);
   12.23 -
   12.24 -
   12.25 -val inductive_casesP =
   12.26 +val _ =
   12.27    OuterSyntax.command "inductive_cases"
   12.28      "create simplified instances of elimination rules (improper)" K.thy_script
   12.29      (P.opt_target -- P.and_list1 SpecParse.spec
   12.30        >> (fn (loc, specs) => Toplevel.local_theory loc (snd o inductive_cases specs)));
   12.31  
   12.32 -val _ = OuterSyntax.add_keywords ["monos"];
   12.33 -val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];
   12.34 -
   12.35  end;
   12.36  
   12.37  end;
    13.1 --- a/src/HOL/Tools/inductive_set_package.ML	Sat Oct 06 16:41:22 2007 +0200
    13.2 +++ b/src/HOL/Tools/inductive_set_package.ML	Sat Oct 06 16:50:04 2007 +0200
    13.3 @@ -543,14 +543,12 @@
    13.4  
    13.5  val ind_set_decl = InductivePackage.gen_ind_decl add_ind_set_def;
    13.6  
    13.7 -val inductive_setP =
    13.8 +val _ =
    13.9    OuterSyntax.command "inductive_set" "define inductive sets" K.thy_decl (ind_set_decl false);
   13.10  
   13.11 -val coinductive_setP =
   13.12 +val _ =
   13.13    OuterSyntax.command "coinductive_set" "define coinductive sets" K.thy_decl (ind_set_decl true);
   13.14  
   13.15 -val _ = OuterSyntax.add_parsers [inductive_setP, coinductive_setP];
   13.16 -
   13.17  end;
   13.18  
   13.19  end;
    14.1 --- a/src/HOL/Tools/primrec_package.ML	Sat Oct 06 16:41:22 2007 +0200
    14.2 +++ b/src/HOL/Tools/primrec_package.ML	Sat Oct 06 16:50:04 2007 +0200
    14.3 @@ -350,15 +350,13 @@
    14.4  val primrec_decl =
    14.5    opt_unchecked_name -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
    14.6  
    14.7 -val primrecP =
    14.8 +val _ =
    14.9    OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
   14.10      (primrec_decl >> (fn ((unchecked, alt_name), eqns) =>
   14.11        Toplevel.theory (snd o
   14.12          (if unchecked then add_primrec_unchecked else add_primrec) alt_name
   14.13            (map P.triple_swap eqns))));
   14.14  
   14.15 -val _ = OuterSyntax.add_parsers [primrecP];
   14.16 -
   14.17  end;
   14.18  
   14.19  end;
    15.1 --- a/src/HOL/Tools/recdef_package.ML	Sat Oct 06 16:41:22 2007 +0200
    15.2 +++ b/src/HOL/Tools/recdef_package.ML	Sat Oct 06 16:50:04 2007 +0200
    15.3 @@ -295,6 +295,8 @@
    15.4  
    15.5  local structure P = OuterParse and K = OuterKeyword in
    15.6  
    15.7 +val _ = OuterSyntax.keywords ["permissive", "congs", "hints"];
    15.8 +
    15.9  val hints =
   15.10    P.$$$ "(" |-- P.!!! (P.position (P.$$$ "hints" -- P.arguments) --| P.$$$ ")") >> Args.src;
   15.11  
   15.12 @@ -303,7 +305,7 @@
   15.13    P.name -- P.term -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop) -- Scan.option hints
   15.14    >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
   15.15  
   15.16 -val recdefP =
   15.17 +val _ =
   15.18    OuterSyntax.command "recdef" "define general recursive functions (TFL)" K.thy_decl
   15.19      (recdef_decl >> Toplevel.theory);
   15.20  
   15.21 @@ -313,21 +315,17 @@
   15.22    Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (SpecParse.xthms1 --| P.$$$ ")")) []
   15.23    >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
   15.24  
   15.25 -val defer_recdefP =
   15.26 +val _ =
   15.27    OuterSyntax.command "defer_recdef" "defer general recursive functions (TFL)" K.thy_decl
   15.28      (defer_recdef_decl >> Toplevel.theory);
   15.29  
   15.30 -val recdef_tcP =
   15.31 +val _ =
   15.32    OuterSyntax.command "recdef_tc" "recommence proof of termination condition (TFL)" K.thy_goal
   15.33      (P.opt_target --
   15.34        SpecParse.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
   15.35        >> (fn (((loc, thm_name), name), i) =>
   15.36          Toplevel.print o Toplevel.local_theory_to_proof' loc (recdef_tc thm_name name i)));
   15.37  
   15.38 -
   15.39 -val _ = OuterSyntax.add_keywords ["permissive", "congs", "hints"];
   15.40 -val _ = OuterSyntax.add_parsers [recdefP, defer_recdefP, recdef_tcP];
   15.41 -
   15.42  end;
   15.43  
   15.44  end;
    16.1 --- a/src/HOL/Tools/record_package.ML	Sat Oct 06 16:41:22 2007 +0200
    16.2 +++ b/src/HOL/Tools/record_package.ML	Sat Oct 06 16:50:04 2007 +0200
    16.3 @@ -607,7 +607,7 @@
    16.4                         val types = map snd flds';
    16.5                         val (args,rest) = splitargs (map fst flds') fargs;
    16.6                         val argtypes = map (Sign.certify_typ thy o decode_type thy) args;
    16.7 -                       val midx =  fold (fn T => fn i => Int.max (maxidx_of_typ T, i)) 
    16.8 +                       val midx =  fold (fn T => fn i => Int.max (maxidx_of_typ T, i))
    16.9                                      argtypes 0;
   16.10                         val varifyT = varifyT midx;
   16.11                         val vartypes = map varifyT types;
   16.12 @@ -654,12 +654,12 @@
   16.13        gen_adv_record_type_scheme_tr "_field_types" "_field_type" ext_typeN;
   16.14  
   16.15  
   16.16 -val parse_translation = 
   16.17 +val parse_translation =
   16.18   [("_record_update", record_update_tr),
   16.19    ("_update_name", update_name_tr)];
   16.20  
   16.21  
   16.22 -val adv_parse_translation = 
   16.23 +val adv_parse_translation =
   16.24   [("_record",adv_record_tr),
   16.25    ("_record_scheme",adv_record_scheme_tr),
   16.26    ("_record_type",adv_record_type_tr),
   16.27 @@ -762,7 +762,7 @@
   16.28            in Syntax.term_of_typ (! Syntax.show_sorts)
   16.29                 (Sign.extern_typ thy (Envir.norm_type subst abbrT)) end;
   16.30  
   16.31 -      fun match rT T = (Sign.typ_match thy (varifyT rT,T) 
   16.32 +      fun match rT T = (Sign.typ_match thy (varifyT rT,T)
   16.33                                                  Vartab.empty);
   16.34  
   16.35     in if !print_record_type_abbr
   16.36 @@ -876,8 +876,8 @@
   16.37       val f_x = Free (f',fT)$(Free (x,T'));
   16.38       fun is_constr (Const (c,_)$_) = can (unsuffix extN) c
   16.39         | is_constr _ = false;
   16.40 -     fun subst (t as u$w) = if Free (f',fT)=u 
   16.41 -                            then if is_constr w then f_x 
   16.42 +     fun subst (t as u$w) = if Free (f',fT)=u
   16.43 +                            then if is_constr w then f_x
   16.44                                   else raise TERM ("abstract_over_fun_app",[t])
   16.45                              else subst u$subst w
   16.46         | subst (Abs (x,T,t)) = (Abs (x,T,subst t))
   16.47 @@ -885,12 +885,12 @@
   16.48       val t'' = abstract_over (f_x,subst t');
   16.49       val vars = strip_qnt_vars "all" t'';
   16.50       val bdy = strip_qnt_body "all" t'';
   16.51 -     
   16.52 +
   16.53    in list_abs ((x,T')::vars,bdy) end
   16.54    | abstract_over_fun_app t = raise TERM ("abstract_over_fun_app",[t]);
   16.55  (* Generates a theorem of the kind:
   16.56 - * !!f x*. PROP P (f ( r x* ) x* == !!r x*. PROP P r x* 
   16.57 - *) 
   16.58 + * !!f x*. PROP P (f ( r x* ) x* == !!r x*. PROP P r x*
   16.59 + *)
   16.60  fun mk_fun_apply_eq (Abs (f, fT, t)) thy =
   16.61    let
   16.62      val rT = domain_type fT;
   16.63 @@ -900,16 +900,16 @@
   16.64      fun app_bounds 0 t = t$Bound 0
   16.65        | app_bounds n t = if n > 0 then app_bounds (n-1) (t$Bound n) else t
   16.66  
   16.67 -   
   16.68 +
   16.69      val [P,r] = Term.variant_frees t [("P",rT::Ts--->Term.propT),("r",Ts--->rT)];
   16.70      val prop = Logic.mk_equals
   16.71                  (list_all ((f,fT)::vars,
   16.72                             app_bounds (n - 1) ((Free P)$(Bound n$app_bounds (n-1) (Free r)))),
   16.73                   list_all ((fst r,rT)::vars,
   16.74 -                           app_bounds (n - 1) ((Free P)$Bound n))); 
   16.75 +                           app_bounds (n - 1) ((Free P)$Bound n)));
   16.76      val prove_standard = quick_and_dirty_prove true thy;
   16.77      val thm = prove_standard [] prop (fn prems =>
   16.78 -	 EVERY [rtac equal_intr_rule 1, 
   16.79 +	 EVERY [rtac equal_intr_rule 1,
   16.80                  Goal.norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1,
   16.81                  Goal.norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1]);
   16.82    in thm end
   16.83 @@ -928,14 +928,14 @@
   16.84                    (trm as Abs _) =>
   16.85           (case rec_id (~1) T of
   16.86              "" => NONE
   16.87 -          | n => if T=T'  
   16.88 +          | n => if T=T'
   16.89                   then (let
   16.90 -                        val P=cterm_of thy (abstract_over_fun_app trm); 
   16.91 +                        val P=cterm_of thy (abstract_over_fun_app trm);
   16.92                          val thm = mk_fun_apply_eq trm thy;
   16.93                          val PV = cterm_of thy (hd (term_vars (prop_of thm)));
   16.94                          val thm' = cterm_instantiate [(PV,P)] thm;
   16.95                         in SOME  thm' end handle TERM _ => NONE)
   16.96 -                else NONE) 
   16.97 +                else NONE)
   16.98         | _ => NONE))
   16.99  end
  16.100  
  16.101 @@ -951,7 +951,7 @@
  16.102                                (* [thm] is the same as all_thm *)
  16.103                   | NONE => extsplits)
  16.104      val thms'=K_comp_convs@thms;
  16.105 -    val ss' = (Simplifier.inherit_context ss simpset 
  16.106 +    val ss' = (Simplifier.inherit_context ss simpset
  16.107                  addsimps thms'
  16.108                  addsimprocs [record_split_f_more_simproc]);
  16.109    in
  16.110 @@ -992,8 +992,8 @@
  16.111                       NONE => NONE
  16.112                     | SOME u_name
  16.113                       => if u_name = s
  16.114 -                        then (case mk_eq_terms r of 
  16.115 -                               NONE => 
  16.116 +                        then (case mk_eq_terms r of
  16.117 +                               NONE =>
  16.118                                   let
  16.119                                     val rv = ("r",rT)
  16.120                                     val rb = Bound 0
  16.121 @@ -1064,7 +1064,7 @@
  16.122                          in ((Const (u,uT)$k$sprout,Const (u,uT)$kb$skeleton),kv::vars) end
  16.123                     else ((sprout,skeleton),vars);
  16.124  
  16.125 -             fun is_upd_same (sprout,skeleton) u 
  16.126 +             fun is_upd_same (sprout,skeleton) u
  16.127                                  ((K_rec as Const ("Record.K_record",_))$
  16.128                                    ((sel as Const (s,_))$r)) =
  16.129                     if (unsuffix updateN u) = s andalso (seed s sprout) = r
  16.130 @@ -1074,17 +1074,17 @@
  16.131  
  16.132               fun init_seed r = ((r,Bound 0), [("r", rT)]);
  16.133  
  16.134 -             fun add (n:string) f fmaps = 
  16.135 +             fun add (n:string) f fmaps =
  16.136                 (case AList.lookup (op =) fmaps n of
  16.137                    NONE => AList.update (op =) (n,[f]) fmaps
  16.138 -                | SOME fs => AList.update (op =) (n,f::fs) fmaps) 
  16.139 +                | SOME fs => AList.update (op =) (n,f::fs) fmaps)
  16.140  
  16.141 -             fun comps (n:string) T fmaps = 
  16.142 +             fun comps (n:string) T fmaps =
  16.143                 (case AList.lookup (op =) fmaps n of
  16.144 -                 SOME fs => 
  16.145 +                 SOME fs =>
  16.146                     foldr1 (fn (f,g) => Const ("Fun.comp",(T-->T)-->(T-->T)-->(T-->T))$f$g) fs
  16.147                  | NONE => error ("record_upd_simproc.comps"))
  16.148 -             
  16.149 +
  16.150               (* mk_updterm returns either
  16.151                *  - Init (orig-term, orig-term-skeleton, vars) if no optimisation can be made,
  16.152                *     where vars are the bound variables in the skeleton
  16.153 @@ -1119,7 +1119,7 @@
  16.154                                     val kv = (n, kT);
  16.155                                     val kb = Bound (length vars);
  16.156                                     val (sprout',vars') = grow u uT k kT (kv::vars) sprout;
  16.157 -                                 in Inter(upd$kb$trm,trm',kv::vars',add n kb fmaps,sprout') 
  16.158 +                                 in Inter(upd$kb$trm,trm',kv::vars',add n kb fmaps,sprout')
  16.159                                   end)
  16.160                           else
  16.161                            (case rest (u::already) r of
  16.162 @@ -1149,7 +1149,7 @@
  16.163                                      val kv = (n, kT)
  16.164                                      val kb = Bound (length vars)
  16.165                                      val (sprout',vars') = grow u uT k kT (kv::vars) sprout
  16.166 -                                    val fmaps' = add n kb fmaps 
  16.167 +                                    val fmaps' = add n kb fmaps
  16.168                                    in Inter (upd$kb$trm,upd$comps n T fmaps'$trm'
  16.169                                             ,vars',fmaps',sprout') end))
  16.170                       end
  16.171 @@ -1161,7 +1161,7 @@
  16.172                  => SOME (prove_split_simp thy ss rT
  16.173                            (list_all(vars,(equals rT$trm$trm'))))
  16.174               | _ => NONE)
  16.175 -         end 
  16.176 +         end
  16.177         | _ => NONE))
  16.178  end
  16.179  
  16.180 @@ -1625,7 +1625,7 @@
  16.181          val refls = map mkrefl fields_more;
  16.182          val dest_convs' = map mk_meta_eq dest_convs;
  16.183          val map_eqs = map (uncurry Thm.combination) (refls ~~ dest_convs');
  16.184 -        
  16.185 +
  16.186          val constr_refl = Thm.reflexive (cterm_of defs_thy (head_of ext));
  16.187  
  16.188          fun mkthm (udef,(fld_refl,thms)) =
  16.189 @@ -1664,7 +1664,7 @@
  16.190      val split_meta = timeit_msg "record extension split_meta proof:" split_meta_prf;
  16.191  
  16.192  
  16.193 -    val (([inject',induct',cases',surjective',split_meta'], 
  16.194 +    val (([inject',induct',cases',surjective',split_meta'],
  16.195            [dest_convs',upd_convs']),
  16.196        thm_thy) =
  16.197        defs_thy
  16.198 @@ -1915,7 +1915,7 @@
  16.199        ||>> ((PureThy.add_defs_i false o map Thm.no_attributes) upd_specs)
  16.200        ||>> ((PureThy.add_defs_i false o map Thm.no_attributes)
  16.201               [make_spec, fields_spec, extend_spec, truncate_spec])
  16.202 -      |-> (fn defs as ((sel_defs, upd_defs), derived_defs) => 
  16.203 +      |-> (fn defs as ((sel_defs, upd_defs), derived_defs) =>
  16.204            fold Code.add_default_func sel_defs
  16.205            #> fold Code.add_default_func upd_defs
  16.206            #> fold Code.add_default_func derived_defs
  16.207 @@ -2276,12 +2276,10 @@
  16.208    P.type_args -- P.name --
  16.209      (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const);
  16.210  
  16.211 -val recordP =  
  16.212 +val _ =
  16.213    OuterSyntax.command "record" "define extensible record" K.thy_decl
  16.214      (record_decl >> (fn (x, (y, z)) => Toplevel.theory (add_record x y z)));
  16.215  
  16.216 -val _ = OuterSyntax.add_parsers [recordP];
  16.217 -
  16.218  end;
  16.219  
  16.220  end;
    17.1 --- a/src/HOL/Tools/refute_isar.ML	Sat Oct 06 16:41:22 2007 +0200
    17.2 +++ b/src/HOL/Tools/refute_isar.ML	Sat Oct 06 16:50:04 2007 +0200
    17.3 @@ -7,7 +7,7 @@
    17.4  syntax.
    17.5  *)
    17.6  
    17.7 -structure RefuteIsar =
    17.8 +structure RefuteIsar: sig end =
    17.9  struct
   17.10  
   17.11  (* ------------------------------------------------------------------------- *)
   17.12 @@ -56,7 +56,7 @@
   17.13  
   17.14  	fun refute_parser tokens = (refute_scan_args tokens) |>> refute_trans;
   17.15  
   17.16 -	val refute_cmd = OuterSyntax.improper_command "refute"
   17.17 +	val _ = OuterSyntax.improper_command "refute"
   17.18  		"try to find a model that refutes a given subgoal"
   17.19  		OuterKeyword.diag refute_parser;
   17.20  
   17.21 @@ -101,15 +101,9 @@
   17.22  	fun refute_params_parser tokens =
   17.23  		(refute_params_scan_args tokens) |>> refute_params_trans;
   17.24  
   17.25 -	val refute_params_cmd = OuterSyntax.command "refute_params"
   17.26 +	val _ = OuterSyntax.command "refute_params"
   17.27  		"show/store default parameters for the 'refute' command"
   17.28  		OuterKeyword.thy_decl refute_params_parser;
   17.29  
   17.30  end;
   17.31  
   17.32 -(* ------------------------------------------------------------------------- *)
   17.33 -(* add the two new commands 'refute' and 'refute_params' to Isabelle/Isar's  *)
   17.34 -(* outer syntax                                                              *)
   17.35 -(* ------------------------------------------------------------------------- *)
   17.36 -
   17.37 -OuterSyntax.add_parsers [RefuteIsar.refute_cmd, RefuteIsar.refute_params_cmd];
    18.1 --- a/src/HOL/Tools/res_atp.ML	Sat Oct 06 16:41:22 2007 +0200
    18.2 +++ b/src/HOL/Tools/res_atp.ML	Sat Oct 06 16:50:04 2007 +0200
    18.3 @@ -969,8 +969,8 @@
    18.4            isar_atp_writeonly (ctxt, chain_ths, goal))
    18.5    end;
    18.6  
    18.7 -val _ = OuterSyntax.add_parsers
    18.8 -  [OuterSyntax.command "sledgehammer" "call automatic theorem provers" OuterKeyword.diag
    18.9 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep sledgehammer))];
   18.10 +val _ =
   18.11 +  OuterSyntax.command "sledgehammer" "call automatic theorem provers" OuterKeyword.diag
   18.12 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep sledgehammer));
   18.13  
   18.14  end;
    19.1 --- a/src/HOL/Tools/specification_package.ML	Sat Oct 06 16:41:22 2007 +0200
    19.2 +++ b/src/HOL/Tools/specification_package.ML	Sat Oct 06 16:50:04 2007 +0200
    19.3 @@ -244,7 +244,7 @@
    19.4    P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
    19.5            Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop)
    19.6  
    19.7 -val specificationP =
    19.8 +val _ =
    19.9    OuterSyntax.command "specification" "define constants by specification" K.thy_goal
   19.10      (specification_decl >> (fn (cos,alt_props) =>
   19.11                                 Toplevel.print o (Toplevel.theory_to_proof
   19.12 @@ -255,14 +255,12 @@
   19.13      (P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
   19.14             Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop))
   19.15  
   19.16 -val ax_specificationP =
   19.17 +val _ =
   19.18    OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal
   19.19      (ax_specification_decl >> (fn (axname,(cos,alt_props)) =>
   19.20                                 Toplevel.print o (Toplevel.theory_to_proof
   19.21                                                       (process_spec (SOME axname) cos alt_props))))
   19.22  
   19.23 -val _ = OuterSyntax.add_parsers [specificationP,ax_specificationP]
   19.24 -
   19.25  end
   19.26  
   19.27  
    20.1 --- a/src/HOL/Tools/typedef_package.ML	Sat Oct 06 16:41:22 2007 +0200
    20.2 +++ b/src/HOL/Tools/typedef_package.ML	Sat Oct 06 16:50:04 2007 +0200
    20.3 @@ -273,7 +273,9 @@
    20.4  
    20.5  local structure P = OuterParse and K = OuterKeyword in
    20.6  
    20.7 -val typedeclP =
    20.8 +val _ = OuterSyntax.keywords ["morphisms"];
    20.9 +
   20.10 +val _ =
   20.11    OuterSyntax.command "typedecl" "type declaration (HOL)" K.thy_decl
   20.12      (P.type_args -- P.name -- P.opt_infix >> (fn ((vs, t), mx) =>
   20.13        Toplevel.theory (add_typedecls [(t, vs, mx)])));
   20.14 @@ -289,14 +291,10 @@
   20.15  fun mk_typedef ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
   20.16    typedef ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
   20.17  
   20.18 -val typedefP =
   20.19 +val _ =
   20.20    OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" K.thy_goal
   20.21      (typedef_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef)));
   20.22  
   20.23 -
   20.24 -val _ = OuterSyntax.add_keywords ["morphisms"];
   20.25 -val _ = OuterSyntax.add_parsers [typedeclP, typedefP];
   20.26 -
   20.27  end;
   20.28  
   20.29  end;
    21.1 --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Sat Oct 06 16:41:22 2007 +0200
    21.2 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Sat Oct 06 16:50:04 2007 +0200
    21.3 @@ -481,10 +481,15 @@
    21.4    add_rename aut source_aut rename_f;
    21.5  
    21.6  
    21.7 -(* parsers *)
    21.8 +(* outer syntax *)
    21.9  
   21.10  local structure P = OuterParse and K = OuterKeyword in
   21.11  
   21.12 +val _ = OuterSyntax.keywords ["signature", "actions", "inputs",
   21.13 +  "outputs", "internals", "states", "initially", "transitions", "pre",
   21.14 +  "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
   21.15 +  "rename"];
   21.16 +
   21.17  val actionlist = P.list1 P.term;
   21.18  val inputslist = P.$$$ "inputs" |-- P.!!! actionlist;
   21.19  val outputslist = P.$$$ "outputs" |-- P.!!! actionlist;
   21.20 @@ -520,21 +525,10 @@
   21.21    (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- (P.!!! (P.name -- (P.$$$ "to" |-- P.term))))))
   21.22      >> mk_rename_decl;
   21.23  
   21.24 -val automatonP =
   21.25 +val _ =
   21.26    OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" K.thy_decl
   21.27      (ioa_decl >> Toplevel.theory);
   21.28  
   21.29  end;
   21.30  
   21.31 -
   21.32 -(* setup outer syntax *)
   21.33 -
   21.34 -val _ = OuterSyntax.add_keywords ["signature", "actions", "inputs",
   21.35 -  "outputs", "internals", "states", "initially", "transitions", "pre",
   21.36 -  "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
   21.37 -  "rename"];
   21.38 -
   21.39 -val _ = OuterSyntax.add_parsers [automatonP];
   21.40 -
   21.41 -
   21.42  end;
    22.1 --- a/src/HOLCF/Tools/cont_consts.ML	Sat Oct 06 16:41:22 2007 +0200
    22.2 +++ b/src/HOLCF/Tools/cont_consts.ML	Sat Oct 06 16:50:04 2007 +0200
    22.3 @@ -99,12 +99,10 @@
    22.4  
    22.5  local structure P = OuterParse and K = OuterKeyword in
    22.6  
    22.7 -val constsP =
    22.8 +val _ =
    22.9    OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl
   22.10      (Scan.repeat1 P.const >> (Toplevel.theory o add_consts));
   22.11  
   22.12 -val _ = OuterSyntax.add_parsers [constsP];
   22.13 -
   22.14  end;
   22.15  
   22.16  end;
    23.1 --- a/src/HOLCF/Tools/domain/domain_extender.ML	Sat Oct 06 16:41:22 2007 +0200
    23.2 +++ b/src/HOLCF/Tools/domain/domain_extender.ML	Sat Oct 06 16:50:04 2007 +0200
    23.3 @@ -146,6 +146,8 @@
    23.4  
    23.5  local structure P = OuterParse and K = OuterKeyword in
    23.6  
    23.7 +val _ = OuterSyntax.keywords ["lazy"];
    23.8 +
    23.9  val dest_decl =
   23.10    P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
   23.11      (P.name >> SOME) -- (P.$$$ "::" |-- P.typ)  --| P.$$$ ")" >> P.triple1
   23.12 @@ -170,14 +172,10 @@
   23.13    >> (fn (opt_name, doms) =>
   23.14        (case opt_name of NONE => space_implode "_" (map (#1 o #1) doms) | SOME s => s, doms));
   23.15  
   23.16 -val domainP =
   23.17 +val _ =
   23.18    OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl
   23.19      (domains_decl >> (Toplevel.theory o add_domain));
   23.20  
   23.21 -
   23.22 -val _ = OuterSyntax.add_keywords ["lazy"];
   23.23 -val _ = OuterSyntax.add_parsers [domainP];
   23.24 -
   23.25 -end; (* local structure *)
   23.26 +end;
   23.27  
   23.28  end;
    24.1 --- a/src/HOLCF/Tools/fixrec_package.ML	Sat Oct 06 16:41:22 2007 +0200
    24.2 +++ b/src/HOLCF/Tools/fixrec_package.ML	Sat Oct 06 16:50:04 2007 +0200
    24.3 @@ -299,19 +299,17 @@
    24.4  
    24.5  (* this builds a parser for a new keyword, fixrec, whose functionality 
    24.6  is defined by add_fixrec *)
    24.7 -val fixrecP =
    24.8 +val _ =
    24.9    OuterSyntax.command "fixrec" "define recursive functions (HOLCF)" K.thy_decl
   24.10      (fixrec_decl >> (Toplevel.theory o uncurry add_fixrec));
   24.11  
   24.12  (* fixpat parser *)
   24.13  val fixpat_decl = SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop;
   24.14  
   24.15 -val fixpatP =
   24.16 +val _ =
   24.17    OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl
   24.18      (fixpat_decl >> (Toplevel.theory o add_fixpat));
   24.19  
   24.20 -val _ = OuterSyntax.add_parsers [fixrecP, fixpatP];
   24.21 +end;
   24.22  
   24.23 -end; (* local structure *)
   24.24 -
   24.25 -end; (* struct *)
   24.26 +end;
    25.1 --- a/src/HOLCF/Tools/pcpodef_package.ML	Sat Oct 06 16:41:22 2007 +0200
    25.2 +++ b/src/HOLCF/Tools/pcpodef_package.ML	Sat Oct 06 16:50:04 2007 +0200
    25.3 @@ -184,7 +184,7 @@
    25.4  
    25.5  local structure P = OuterParse and K = OuterKeyword in
    25.6  
    25.7 -(* copied from HOL/Tools/typedef_package.ML *)
    25.8 +(* cf. HOL/Tools/typedef_package.ML *)
    25.9  val typedef_proof_decl =
   25.10    Scan.optional (P.$$$ "(" |--
   25.11        ((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s)))
   25.12 @@ -196,18 +196,16 @@
   25.13    (if pcpo then pcpodef_proof else cpodef_proof)
   25.14      ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
   25.15  
   25.16 -val pcpodefP =
   25.17 +val _ =
   25.18    OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
   25.19      (typedef_proof_decl >>
   25.20        (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)));
   25.21  
   25.22 -val cpodefP =
   25.23 +val _ =
   25.24    OuterSyntax.command "cpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
   25.25      (typedef_proof_decl >>
   25.26        (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)));
   25.27  
   25.28 -val _ = OuterSyntax.add_parsers [pcpodefP, cpodefP];
   25.29 -
   25.30  end;
   25.31  
   25.32  end;
    26.1 --- a/src/Provers/classical.ML	Sat Oct 06 16:41:22 2007 +0200
    26.2 +++ b/src/Provers/classical.ML	Sat Oct 06 16:50:04 2007 +0200
    26.3 @@ -1084,7 +1084,7 @@
    26.4  
    26.5  (** outer syntax **)
    26.6  
    26.7 -val print_clasetP =
    26.8 +val _ =
    26.9    OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner"
   26.10      OuterKeyword.diag
   26.11      (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep
   26.12 @@ -1092,7 +1092,4 @@
   26.13          (Context.cases print_claset print_local_claset)
   26.14          (print_local_claset o Proof.context_of)))));
   26.15  
   26.16 -val _ = OuterSyntax.add_parsers [print_clasetP];
   26.17 -
   26.18 -
   26.19  end;
    27.1 --- a/src/Pure/Proof/extraction.ML	Sat Oct 06 16:41:22 2007 +0200
    27.2 +++ b/src/Pure/Proof/extraction.ML	Sat Oct 06 16:50:04 2007 +0200
    27.3 @@ -759,7 +759,7 @@
    27.4  
    27.5  val parse_vars = Scan.optional (P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") [];
    27.6  
    27.7 -val realizersP =
    27.8 +val _ =
    27.9    OuterSyntax.command "realizers"
   27.10    "specify realizers for primitive axioms / theorems, together with correctness proof"
   27.11    K.thy_decl
   27.12 @@ -768,23 +768,21 @@
   27.13         (map (fn (((a, vs), s1), s2) =>
   27.14           (PureThy.get_thm thy (Name a), (vs, s1, s2))) xs) thy)));
   27.15  
   27.16 -val realizabilityP =
   27.17 +val _ =
   27.18    OuterSyntax.command "realizability"
   27.19    "add equations characterizing realizability" K.thy_decl
   27.20    (Scan.repeat1 P.string >> (Toplevel.theory o add_realizes_eqns));
   27.21  
   27.22 -val typeofP =
   27.23 +val _ =
   27.24    OuterSyntax.command "extract_type"
   27.25    "add equations characterizing type of extracted program" K.thy_decl
   27.26    (Scan.repeat1 P.string >> (Toplevel.theory o add_typeof_eqns));
   27.27  
   27.28 -val extractP =
   27.29 +val _ =
   27.30    OuterSyntax.command "extract" "extract terms from proofs" K.thy_decl
   27.31      (Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory
   27.32        (fn thy => extract (map (apfst (PureThy.get_thm thy o Name)) xs) thy)));
   27.33  
   27.34 -val _ = OuterSyntax.add_parsers [realizersP, realizabilityP, typeofP, extractP];
   27.35 -
   27.36  val etype_of = etype_of o add_syntax;
   27.37  
   27.38  end;
    28.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Oct 06 16:41:22 2007 +0200
    28.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Oct 06 16:50:04 2007 +0200
    28.3 @@ -231,36 +231,36 @@
    28.4  
    28.5  local structure P = OuterParse and K = OuterKeyword in
    28.6  
    28.7 -val undoP = (*undo without output*)
    28.8 +fun undoP () = (*undo without output*)
    28.9    OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
   28.10      (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
   28.11  
   28.12 -val restartP =
   28.13 +fun restartP () =
   28.14    OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
   28.15      (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
   28.16  
   28.17 -val kill_proofP =
   28.18 +fun kill_proofP () =
   28.19    OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
   28.20      (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
   28.21  
   28.22 -val inform_file_processedP =
   28.23 +fun inform_file_processedP () =
   28.24    OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
   28.25      (P.name >> (fn file => Toplevel.no_timing o
   28.26        Toplevel.init_empty (vacuous_inform_file_processed file) o
   28.27        Toplevel.kill o
   28.28        Toplevel.init_empty (proper_inform_file_processed file)));
   28.29  
   28.30 -val inform_file_retractedP =
   28.31 +fun inform_file_retractedP () =
   28.32    OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
   28.33      (P.name >> (Toplevel.no_timing oo
   28.34        (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
   28.35  
   28.36 -val process_pgipP =
   28.37 +fun process_pgipP () =
   28.38    OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
   28.39      (P.text >> (Toplevel.no_timing oo
   28.40        (fn txt => Toplevel.imperative (fn () => ProofGeneralPgip.process_pgip txt))));
   28.41  
   28.42 -fun init_outer_syntax () = OuterSyntax.add_parsers
   28.43 +fun init_outer_syntax () = List.app (fn f => f ())
   28.44   [undoP, restartP, kill_proofP, inform_file_processedP, inform_file_retractedP, process_pgipP];
   28.45  
   28.46  end;
    29.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Oct 06 16:41:22 2007 +0200
    29.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Oct 06 16:50:04 2007 +0200
    29.3 @@ -1125,21 +1125,13 @@
    29.4  end
    29.5  
    29.6  
    29.7 -local
    29.8  (* Extra command for embedding prover-control inside document (obscure/debug usage). *)
    29.9  
   29.10 -val process_pgipP =
   29.11 +fun init_outer_syntax () =
   29.12    OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" OuterKeyword.control
   29.13      (OuterParse.text >> (Toplevel.no_timing oo
   29.14        (fn txt => Toplevel.imperative (fn () => process_pgip_plain txt))));
   29.15  
   29.16 -in
   29.17 -
   29.18 - fun init_outer_syntax () = OuterSyntax.add_parsers [process_pgipP];
   29.19 -
   29.20 -end
   29.21 -
   29.22 -
   29.23  
   29.24  (* init *)
   29.25  
    30.1 --- a/src/Pure/Tools/invoke.ML	Sat Oct 06 16:41:22 2007 +0200
    30.2 +++ b/src/Pure/Tools/invoke.ML	Sat Oct 06 16:50:04 2007 +0200
    30.3 @@ -115,7 +115,7 @@
    30.4  
    30.5  local structure P = OuterParse and K = OuterKeyword in
    30.6  
    30.7 -val invokeP =
    30.8 +val _ =
    30.9    OuterSyntax.command "invoke"
   30.10      "schematic invocation of locale expression in proof context"
   30.11      (K.tag_proof K.prf_goal)
   30.12 @@ -123,8 +123,6 @@
   30.13        >> (fn (((name, expr), (insts, _)), fixes) =>
   30.14            Toplevel.print o Toplevel.proof' (invoke name expr insts fixes)));
   30.15  
   30.16 -val _ = OuterSyntax.add_parsers [invokeP];
   30.17 -
   30.18  end;
   30.19  
   30.20  end;
    31.1 --- a/src/Pure/Tools/named_thms.ML	Sat Oct 06 16:41:22 2007 +0200
    31.2 +++ b/src/Pure/Tools/named_thms.ML	Sat Oct 06 16:50:04 2007 +0200
    31.3 @@ -36,10 +36,10 @@
    31.4  val setup =
    31.5    Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)];
    31.6  
    31.7 -val _ = OuterSyntax.add_parsers
    31.8 - [OuterSyntax.improper_command ("print_" ^ name ^ "_rules") ("print " ^ description)
    31.9 +val _ =
   31.10 +  OuterSyntax.improper_command ("print_" ^ name ^ "_rules") ("print " ^ description)
   31.11      OuterKeyword.diag
   31.12      (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
   31.13 -      Toplevel.keep (Pretty.writeln o pretty o Toplevel.context_of)))];
   31.14 +      Toplevel.keep (Pretty.writeln o pretty o Toplevel.context_of)));
   31.15  
   31.16  end;
    32.1 --- a/src/Pure/codegen.ML	Sat Oct 06 16:41:22 2007 +0200
    32.2 +++ b/src/Pure/codegen.ML	Sat Oct 06 16:50:04 2007 +0200
    32.3 @@ -1100,6 +1100,8 @@
    32.4  
    32.5  structure P = OuterParse and K = OuterKeyword;
    32.6  
    32.7 +val _ = OuterSyntax.keywords ["attach", "file", "contains"];
    32.8 +
    32.9  fun strip_whitespace s = implode (fst (take_suffix (equal "\n" orf equal " ")
   32.10    (snd (take_prefix (equal "\n" orf equal " ") (explode s))))) ^ "\n";
   32.11  
   32.12 @@ -1107,7 +1109,7 @@
   32.13    Scan.optional (P.$$$ "(" |-- P.xname --| P.$$$ ")") "" --
   32.14      (P.verbatim >> strip_whitespace));
   32.15  
   32.16 -val assoc_typeP =
   32.17 +val _ =
   32.18    OuterSyntax.command "types_code"
   32.19    "associate types with target language types" K.thy_decl
   32.20      (Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
   32.21 @@ -1115,7 +1117,7 @@
   32.22         (fn ((name, mfx), aux) => (name, (parse_mixfix
   32.23           (Syntax.read_typ_global thy) mfx, aux)))) xs thy)));
   32.24  
   32.25 -val assoc_constP =
   32.26 +val _ =
   32.27    OuterSyntax.command "consts_code"
   32.28    "associate constants with target language code" K.thy_decl
   32.29      (Scan.repeat1
   32.30 @@ -1152,12 +1154,12 @@
   32.31             else map_modules (Symtab.update (module, gr)) thy)
   32.32       end));
   32.33  
   32.34 -val code_libraryP =
   32.35 +val _ =
   32.36    OuterSyntax.command "code_library"
   32.37      "generates code for terms (one structure for each theory)" K.thy_decl
   32.38      (parse_code true);
   32.39  
   32.40 -val code_moduleP =
   32.41 +val _ =
   32.42    OuterSyntax.command "code_module"
   32.43      "generates code for terms (single structure, incremental)" K.thy_decl
   32.44      (parse_code false);
   32.45 @@ -1174,13 +1176,13 @@
   32.46    (P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn thy =>
   32.47      fn (x, ys) => (x, (v, Syntax.read_typ_global thy s) :: ys))) xs;
   32.48  
   32.49 -val test_paramsP =
   32.50 +val _ =
   32.51    OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl
   32.52      (P.$$$ "[" |-- P.list1 parse_test_params --| P.$$$ "]" >>
   32.53        (fn fs => Toplevel.theory (fn thy =>
   32.54           map_test_params (Library.apply (map (fn f => f thy) fs)) thy)));
   32.55  
   32.56 -val testP =
   32.57 +val _ =
   32.58    OuterSyntax.command "quickcheck" "try to find counterexample for subgoal" K.diag
   32.59    (Scan.option (P.$$$ "[" |-- P.list1
   32.60      (   parse_test_params >> (fn f => fn thy => apfst (f thy))
   32.61 @@ -1191,15 +1193,10 @@
   32.62          (get_test_params (Toplevel.theory_of st), [])) g [] |>
   32.63        pretty_counterex (Toplevel.context_of st) |> Pretty.writeln)));
   32.64  
   32.65 -val valueP =
   32.66 +val _ =
   32.67    OuterSyntax.improper_command "value" "read, evaluate and print term" K.diag
   32.68      (P.term >> (Toplevel.no_timing oo print_evaluated_term));
   32.69  
   32.70 -val _ = OuterSyntax.add_keywords ["attach", "file", "contains"];
   32.71 -
   32.72 -val _ = OuterSyntax.add_parsers
   32.73 -  [assoc_typeP, assoc_constP, code_libraryP, code_moduleP, test_paramsP, testP, valueP];
   32.74 -
   32.75  end;
   32.76  
   32.77  val auto_quickcheck = Codegen.auto_quickcheck;
    33.1 --- a/src/Tools/code/code_package.ML	Sat Oct 06 16:41:22 2007 +0200
    33.2 +++ b/src/Tools/code/code_package.ML	Sat Oct 06 16:50:04 2007 +0200
    33.3 @@ -558,14 +558,14 @@
    33.4       -- Scan.optional (P.$$$ "(" |-- P.arguments --| P.$$$ ")") []
    33.5    ) >> (fn (raw_cs, seris) => cmd raw_cs seris));
    33.6  
    33.7 -val _ = OuterSyntax.add_keywords [inK, module_nameK, fileK];
    33.8 +val _ = OuterSyntax.keywords [inK, module_nameK, fileK];
    33.9  
   33.10  val (codeK, code_thmsK, code_depsK, code_propsK) =
   33.11    ("export_code", "code_thms", "code_deps", "code_props");
   33.12  
   33.13  in
   33.14  
   33.15 -val codeP =
   33.16 +val _ =
   33.17    OuterSyntax.improper_command codeK "generate executable code for constants"
   33.18      K.diag (P.!!! (code_exprP code_cmd) >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
   33.19  
   33.20 @@ -574,24 +574,22 @@
   33.21     of SOME f => (writeln "Now generating code..."; f thy)
   33.22      | NONE => error ("Bad directive " ^ quote cmd);
   33.23  
   33.24 -val code_thmsP =
   33.25 +val _ =
   33.26    OuterSyntax.improper_command code_thmsK "print system of defining equations for code" OuterKeyword.diag
   33.27      (Scan.repeat P.term
   33.28        >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
   33.29          o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
   33.30  
   33.31 -val code_depsP =
   33.32 +val _ =
   33.33    OuterSyntax.improper_command code_depsK "visualize dependencies of defining equations for code" OuterKeyword.diag
   33.34      (Scan.repeat P.term
   33.35        >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
   33.36          o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
   33.37  
   33.38 -val code_propsP =
   33.39 +val _ =
   33.40    OuterSyntax.command code_propsK "generate characteristic properties for executable constants"
   33.41      K.thy_decl (P.!!! (code_exprP code_props_cmd) >> Toplevel.theory);
   33.42  
   33.43 -val _ = OuterSyntax.add_parsers [codeP, code_thmsP, code_depsP, code_propsP];
   33.44 -
   33.45  end; (*local*)
   33.46  
   33.47  end; (*struct*)
    34.1 --- a/src/Tools/code/code_target.ML	Sat Oct 06 16:41:22 2007 +0200
    34.2 +++ b/src/Tools/code/code_target.ML	Sat Oct 06 16:50:04 2007 +0200
    34.3 @@ -2091,7 +2091,10 @@
    34.4  
    34.5  val add_haskell_monad = gen_add_haskell_monad CodeUnit.read_const;
    34.6  
    34.7 -val code_classP =
    34.8 +
    34.9 +val _ = OuterSyntax.keywords [infixK, infixlK, infixrK];
   34.10 +
   34.11 +val _ =
   34.12    OuterSyntax.command code_classK "define code syntax for class" K.thy_decl (
   34.13      parse_multi_syntax P.xname
   34.14        (Scan.option (P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
   34.15 @@ -2100,7 +2103,7 @@
   34.16            fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)
   34.17    );
   34.18  
   34.19 -val code_instanceP =
   34.20 +val _ =
   34.21    OuterSyntax.command code_instanceK "define code syntax for instance" K.thy_decl (
   34.22      parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname)
   34.23        ((P.minus >> K true) || Scan.succeed false)
   34.24 @@ -2108,55 +2111,50 @@
   34.25            fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns)
   34.26    );
   34.27  
   34.28 -val code_typeP =
   34.29 +val _ =
   34.30    OuterSyntax.command code_typeK "define code syntax for type constructor" K.thy_decl (
   34.31      parse_multi_syntax P.xname (parse_syntax I)
   34.32      >> (Toplevel.theory oo fold) (fn (target, syns) =>
   34.33            fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns)
   34.34    );
   34.35  
   34.36 -val code_constP =
   34.37 +val _ =
   34.38    OuterSyntax.command code_constK "define code syntax for constant" K.thy_decl (
   34.39      parse_multi_syntax P.term (parse_syntax fst)
   34.40      >> (Toplevel.theory oo fold) (fn (target, syns) =>
   34.41            fold (fn (raw_const, syn) => add_syntax_const_cmd target raw_const (no_bindings syn)) syns)
   34.42    );
   34.43  
   34.44 -val code_monadP =
   34.45 +val _ =
   34.46    OuterSyntax.command code_monadK "define code syntax for Haskell monads" K.thy_decl (
   34.47      P.term -- P.term -- P.term
   34.48      >> (fn ((raw_run, raw_mbind), raw_kbind) => Toplevel.theory 
   34.49            (add_haskell_monad raw_run raw_mbind raw_kbind))
   34.50    );
   34.51  
   34.52 -val code_reservedP =
   34.53 +val _ =
   34.54    OuterSyntax.command code_reservedK "declare words as reserved for target language" K.thy_decl (
   34.55      P.name -- Scan.repeat1 P.name
   34.56      >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds)
   34.57    );
   34.58  
   34.59 -val code_modulenameP =
   34.60 +val _ =
   34.61    OuterSyntax.command code_modulenameK "alias module to other name" K.thy_decl (
   34.62      P.name -- Scan.repeat1 (P.name -- P.name)
   34.63      >> (fn (target, modlnames) => (Toplevel.theory o fold (add_modl_alias target)) modlnames)
   34.64    );
   34.65  
   34.66 -val code_moduleprologP =
   34.67 +val _ =
   34.68    OuterSyntax.command code_moduleprologK "add prolog to module" K.thy_decl (
   34.69      P.name -- Scan.repeat1 (P.name -- (P.text >> (fn "-" => NONE | s => SOME s)))
   34.70      >> (fn (target, prologs) => (Toplevel.theory o fold (add_modl_prolog target)) prologs)
   34.71    );
   34.72  
   34.73 -val code_exceptionP =
   34.74 +val _ =
   34.75    OuterSyntax.command code_exceptionK "permit exceptions for constant" K.thy_decl (
   34.76      Scan.repeat1 P.term >> (Toplevel.theory o fold allow_exception_cmd)
   34.77    );
   34.78  
   34.79 -val _ = OuterSyntax.add_keywords [infixK, infixlK, infixrK];
   34.80 -
   34.81 -val _ = OuterSyntax.add_parsers [code_classP, code_instanceP, code_typeP, code_constP,
   34.82 -  code_reservedP, code_modulenameP, code_moduleprologP, code_monadP, code_exceptionP];
   34.83 -
   34.84  
   34.85  (*including serializer defaults*)
   34.86  val setup =
    35.1 --- a/src/Tools/induct.ML	Sat Oct 06 16:41:22 2007 +0200
    35.2 +++ b/src/Tools/induct.ML	Sat Oct 06 16:50:04 2007 +0200
    35.3 @@ -161,10 +161,10 @@
    35.4      |> Pretty.chunks |> Pretty.writeln
    35.5    end;
    35.6  
    35.7 -val _ = OuterSyntax.add_parsers [
    35.8 +val _ =
    35.9    OuterSyntax.improper_command "print_induct_rules" "print induction and cases rules"
   35.10      OuterKeyword.diag (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
   35.11 -      Toplevel.keep (print_rules o Toplevel.context_of)))];
   35.12 +      Toplevel.keep (print_rules o Toplevel.context_of)));
   35.13  
   35.14  
   35.15  (* access rules *)
    36.1 --- a/src/Tools/nbe.ML	Sat Oct 06 16:41:22 2007 +0200
    36.2 +++ b/src/Tools/nbe.ML	Sat Oct 06 16:50:04 2007 +0200
    36.3 @@ -410,12 +410,10 @@
    36.4  
    36.5  val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
    36.6  
    36.7 -val nbeP =
    36.8 +val _ =
    36.9    OuterSyntax.improper_command "normal_form" "normalize term by evaluation" K.diag
   36.10      (opt_modes -- P.typ >> (Toplevel.keep o norm_print_term_cmd));
   36.11  
   36.12 -val _ = OuterSyntax.add_parsers [nbeP];
   36.13 -
   36.14  end;
   36.15  
   36.16  end;
    37.1 --- a/src/ZF/Tools/datatype_package.ML	Sat Oct 06 16:41:22 2007 +0200
    37.2 +++ b/src/ZF/Tools/datatype_package.ML	Sat Oct 06 16:50:04 2007 +0200
    37.3 @@ -422,11 +422,9 @@
    37.4  
    37.5  val coind_prefix = if coind then "co" else "";
    37.6  
    37.7 -val inductiveP = OuterSyntax.command (coind_prefix ^ "datatype")
    37.8 +val _ = OuterSyntax.command (coind_prefix ^ "datatype")
    37.9    ("define " ^ coind_prefix ^ "datatype") K.thy_decl datatype_decl;
   37.10  
   37.11 -val _ = OuterSyntax.add_parsers [inductiveP];
   37.12 -
   37.13  end;
   37.14  
   37.15  end;
    38.1 --- a/src/ZF/Tools/ind_cases.ML	Sat Oct 06 16:41:22 2007 +0200
    38.2 +++ b/src/ZF/Tools/ind_cases.ML	Sat Oct 06 16:50:04 2007 +0200
    38.3 @@ -76,15 +76,11 @@
    38.4  
    38.5  local structure P = OuterParse and K = OuterKeyword in
    38.6  
    38.7 -val ind_cases =
    38.8 -  P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop)
    38.9 -  >> (Toplevel.theory o inductive_cases);
   38.10 -
   38.11 -val inductive_casesP =
   38.12 +val _ =
   38.13    OuterSyntax.command "inductive_cases"
   38.14 -    "create simplified instances of elimination rules (improper)" K.thy_script ind_cases;
   38.15 -
   38.16 -val _ = OuterSyntax.add_parsers [inductive_casesP];
   38.17 +    "create simplified instances of elimination rules (improper)" K.thy_script
   38.18 +    (P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop)
   38.19 +      >> (Toplevel.theory o inductive_cases));
   38.20  
   38.21  end;
   38.22  
    39.1 --- a/src/ZF/Tools/induct_tacs.ML	Sat Oct 06 16:41:22 2007 +0200
    39.2 +++ b/src/ZF/Tools/induct_tacs.ML	Sat Oct 06 16:50:04 2007 +0200
    39.3 @@ -188,6 +188,8 @@
    39.4  
    39.5  local structure P = OuterParse and K = OuterKeyword in
    39.6  
    39.7 +val _ = OuterSyntax.keywords ["elimination", "induction", "case_eqns", "recursor_eqns"];
    39.8 +
    39.9  val rep_datatype_decl =
   39.10    (P.$$$ "elimination" |-- P.!!! SpecParse.xthm) --
   39.11    (P.$$$ "induction" |-- P.!!! SpecParse.xthm) --
   39.12 @@ -195,13 +197,10 @@
   39.13    Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! SpecParse.xthms1) []
   39.14    >> (fn (((x, y), z), w) => rep_datatype x y z w);
   39.15  
   39.16 -val rep_datatypeP =
   39.17 +val _ =
   39.18    OuterSyntax.command "rep_datatype" "represent existing set inductively" K.thy_decl
   39.19      (rep_datatype_decl >> Toplevel.theory);
   39.20  
   39.21 -val _ = OuterSyntax.add_keywords ["elimination", "induction", "case_eqns", "recursor_eqns"];
   39.22 -val _ = OuterSyntax.add_parsers [rep_datatypeP];
   39.23 -
   39.24  end;
   39.25  
   39.26  end;
    40.1 --- a/src/ZF/Tools/inductive_package.ML	Sat Oct 06 16:41:22 2007 +0200
    40.2 +++ b/src/ZF/Tools/inductive_package.ML	Sat Oct 06 16:50:04 2007 +0200
    40.3 @@ -576,6 +576,9 @@
    40.4  
    40.5  local structure P = OuterParse and K = OuterKeyword in
    40.6  
    40.7 +val _ = OuterSyntax.keywords
    40.8 +  ["domains", "intros", "monos", "con_defs", "type_intros", "type_elims"];
    40.9 +
   40.10  fun mk_ind (((((doms, intrs), monos), con_defs), type_intrs), type_elims) =
   40.11    #1 o add_inductive doms (map P.triple_swap intrs) (monos, con_defs, type_intrs, type_elims);
   40.12  
   40.13 @@ -590,13 +593,9 @@
   40.14    Scan.optional (P.$$$ "type_elims" |-- P.!!! SpecParse.xthms1) []
   40.15    >> (Toplevel.theory o mk_ind);
   40.16  
   40.17 -val inductiveP = OuterSyntax.command (co_prefix ^ "inductive")
   40.18 +val _ = OuterSyntax.command (co_prefix ^ "inductive")
   40.19    ("define " ^ co_prefix ^ "inductive sets") K.thy_decl ind_decl;
   40.20  
   40.21 -val _ = OuterSyntax.add_keywords
   40.22 -  ["domains", "intros", "monos", "con_defs", "type_intros", "type_elims"];
   40.23 -val _ = OuterSyntax.add_parsers [inductiveP];
   40.24 -
   40.25  end;
   40.26  
   40.27  end;
    41.1 --- a/src/ZF/Tools/primrec_package.ML	Sat Oct 06 16:41:22 2007 +0200
    41.2 +++ b/src/ZF/Tools/primrec_package.ML	Sat Oct 06 16:50:04 2007 +0200
    41.3 @@ -203,18 +203,12 @@
    41.4  
    41.5  (* outer syntax *)
    41.6  
    41.7 -local structure P = OuterParse and K = OuterKeyword in
    41.8 -
    41.9 -val primrec_decl = Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
   41.10 +structure P = OuterParse and K = OuterKeyword;
   41.11  
   41.12 -val primrecP =
   41.13 +val _ =
   41.14    OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
   41.15 -    (primrec_decl >> (Toplevel.theory o (#1 oo (add_primrec o map P.triple_swap))));
   41.16 -
   41.17 -val _ = OuterSyntax.add_parsers [primrecP];
   41.18 +    (Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop)
   41.19 +      >> (Toplevel.theory o (#1 oo (add_primrec o map P.triple_swap))));
   41.20  
   41.21  end;
   41.22  
   41.23 -end;
   41.24 -
   41.25 -
    42.1 --- a/src/ZF/Tools/typechk.ML	Sat Oct 06 16:41:22 2007 +0200
    42.2 +++ b/src/ZF/Tools/typechk.ML	Sat Oct 06 16:50:04 2007 +0200
    42.3 @@ -118,10 +118,10 @@
    42.4       Args.del -- Args.colon >> K (I, TC_del)]
    42.5    (fn ctxt => Method.SIMPLE_METHOD (CHANGED (typecheck_tac ctxt)));
    42.6  
    42.7 -val _ = OuterSyntax.add_parsers
    42.8 -  [OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag
    42.9 +val _ =
   42.10 +  OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag
   42.11      (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
   42.12 -      Toplevel.keep (print_tcset o Toplevel.context_of)))];
   42.13 +      Toplevel.keep (print_tcset o Toplevel.context_of)));
   42.14  
   42.15  
   42.16  (* theory setup *)