@{command_spec} is superseded by @{command_keyword};
authorwenzelm
Mon Apr 06 17:06:48 2015 +0200 (2015-04-06)
changeset 59936b8ffc3dc9e24
parent 59935 343905de27b1
child 59937 6eccb133d4e6
@{command_spec} is superseded by @{command_keyword};
NEWS
src/HOL/Decision_Procs/approximation.ML
src/HOL/HOLCF/Tools/Domain/domain.ML
src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOL/HOLCF/Tools/cpodef.ML
src/HOL/HOLCF/Tools/domaindef.ML
src/HOL/HOLCF/Tools/fixrec.ML
src/HOL/Import/import_data.ML
src/HOL/Import/import_rule.ML
src/HOL/Library/Old_SMT/old_smt_config.ML
src/HOL/Library/bnf_axiomatization.ML
src/HOL/Library/code_test.ML
src/HOL/Library/refute.ML
src/HOL/Library/simps_case_conv.ML
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Orderings.thy
src/HOL/SMT_Examples/boogie.ML
src/HOL/SPARK/Tools/spark_commands.ML
src/HOL/Statespace/state_space.ML
src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML
src/HOL/Tools/BNF/bnf_def.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_gfp.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_lfp.ML
src/HOL/Tools/BNF/bnf_lfp_compat.ML
src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
src/HOL/Tools/Ctr_Sugar/case_translation.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/Function/fun.ML
src/HOL/Tools/Function/fun_cases.ML
src/HOL/Tools/Function/function.ML
src/HOL/Tools/Function/partial_function.ML
src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/Lifting/lifting_info.ML
src/HOL/Tools/Lifting/lifting_setup.ML
src/HOL/Tools/Nitpick/nitpick_commands.ML
src/HOL/Tools/Old_Datatype/old_datatype.ML
src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Predicate_Compile/predicate_compile.ML
src/HOL/Tools/Quickcheck/abstract_generators.ML
src/HOL/Tools/Quickcheck/find_unused_assms.ML
src/HOL/Tools/Quotient/quotient_def.ML
src/HOL/Tools/Quotient/quotient_info.ML
src/HOL/Tools/Quotient/quotient_type.ML
src/HOL/Tools/SMT/smt_config.ML
src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
src/HOL/Tools/choice_specification.ML
src/HOL/Tools/functor.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/recdef.ML
src/HOL/Tools/record.ML
src/HOL/Tools/try0.ML
src/HOL/Tools/typedef.ML
src/HOL/Tools/value.ML
src/HOL/ex/Cartouche_Examples.thy
src/HOL/ex/Commands.thy
src/Provers/classical.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/isar_syn.ML
src/Pure/ML/ml_antiquotations.ML
src/Pure/Tools/class_deps.ML
src/Pure/Tools/find_consts.ML
src/Pure/Tools/find_theorems.ML
src/Pure/Tools/named_theorems.ML
src/Pure/Tools/thm_deps.ML
src/Sequents/prover.ML
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_runtime.ML
src/Tools/Code/code_target.ML
src/Tools/Code/code_thingol.ML
src/Tools/adhoc_overloading.ML
src/Tools/induct.ML
src/Tools/permanent_interpretation.ML
src/Tools/quickcheck.ML
src/Tools/solve_direct.ML
src/Tools/subtyping.ML
src/Tools/try.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	Mon Apr 06 16:30:44 2015 +0200
     1.2 +++ b/NEWS	Mon Apr 06 17:06:48 2015 +0200
     1.3 @@ -407,6 +407,10 @@
     1.4  * Goal.prove_multi is superseded by the fully general Goal.prove_common,
     1.5  which also allows to specify a fork priority.
     1.6  
     1.7 +* Antiquotation @{command_spec "COMMAND"} is superseded by
     1.8 +@{command_keyword COMMAND} (usually without quotes and with PIDE
     1.9 +markup). Minor INCOMPATIBILITY.
    1.10 +
    1.11  
    1.12  *** System ***
    1.13  
     2.1 --- a/src/HOL/Decision_Procs/approximation.ML	Mon Apr 06 16:30:44 2015 +0200
     2.2 +++ b/src/HOL/Decision_Procs/approximation.ML	Mon Apr 06 17:06:48 2015 +0200
     2.3 @@ -244,7 +244,7 @@
     2.4    Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
     2.5  
     2.6  val _ =
     2.7 -  Outer_Syntax.command @{command_spec "approximate"} "print approximation of term"
     2.8 +  Outer_Syntax.command @{command_keyword approximate} "print approximation of term"
     2.9      (opt_modes -- Parse.term
    2.10        >> (fn (modes, t) => Toplevel.keep (approximate_cmd modes t)));
    2.11  
     3.1 --- a/src/HOL/HOLCF/Tools/Domain/domain.ML	Mon Apr 06 16:30:44 2015 +0200
     3.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain.ML	Mon Apr 06 17:06:48 2015 +0200
     3.3 @@ -261,7 +261,7 @@
     3.4    end
     3.5  
     3.6  val _ =
     3.7 -  Outer_Syntax.command @{command_spec "domain"} "define recursive domains (HOLCF)"
     3.8 +  Outer_Syntax.command @{command_keyword domain} "define recursive domains (HOLCF)"
     3.9      (domains_decl >> (Toplevel.theory o mk_domain))
    3.10  
    3.11  end
     4.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon Apr 06 16:30:44 2015 +0200
     4.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon Apr 06 17:06:48 2015 +0200
     4.3 @@ -755,7 +755,7 @@
     4.4  in
     4.5  
     4.6  val _ =
     4.7 -  Outer_Syntax.command @{command_spec "domain_isomorphism"} "define domain isomorphisms (HOLCF)"
     4.8 +  Outer_Syntax.command @{command_keyword domain_isomorphism} "define domain isomorphisms (HOLCF)"
     4.9      (parse_domain_isos >> (Toplevel.theory o domain_isomorphism_cmd))
    4.10  
    4.11  end
     5.1 --- a/src/HOL/HOLCF/Tools/cpodef.ML	Mon Apr 06 16:30:44 2015 +0200
     5.2 +++ b/src/HOL/HOLCF/Tools/cpodef.ML	Mon Apr 06 17:06:48 2015 +0200
     5.3 @@ -332,12 +332,12 @@
     5.4      ((t, args, mx), A, morphs)
     5.5  
     5.6  val _ =
     5.7 -  Outer_Syntax.command @{command_spec "pcpodef"}
     5.8 +  Outer_Syntax.command @{command_keyword pcpodef}
     5.9      "HOLCF type definition (requires admissibility proof)"
    5.10      (typedef_proof_decl >> (Toplevel.theory_to_proof o mk_pcpodef_proof true))
    5.11  
    5.12  val _ =
    5.13 -  Outer_Syntax.command @{command_spec "cpodef"}
    5.14 +  Outer_Syntax.command @{command_keyword cpodef}
    5.15      "HOLCF type definition (requires admissibility proof)"
    5.16      (typedef_proof_decl >> (Toplevel.theory_to_proof o mk_pcpodef_proof false))
    5.17  
     6.1 --- a/src/HOL/HOLCF/Tools/domaindef.ML	Mon Apr 06 16:30:44 2015 +0200
     6.2 +++ b/src/HOL/HOLCF/Tools/domaindef.ML	Mon Apr 06 17:06:48 2015 +0200
     6.3 @@ -209,7 +209,7 @@
     6.4    domaindef_cmd ((t, args, mx), A, morphs)
     6.5  
     6.6  val _ =
     6.7 -  Outer_Syntax.command @{command_spec "domaindef"} "HOLCF definition of domains from deflations"
     6.8 +  Outer_Syntax.command @{command_keyword domaindef} "HOLCF definition of domains from deflations"
     6.9      (domaindef_decl >> (Toplevel.theory o mk_domaindef))
    6.10  
    6.11  end
     7.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Mon Apr 06 16:30:44 2015 +0200
     7.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Mon Apr 06 17:06:48 2015 +0200
     7.3 @@ -399,7 +399,7 @@
     7.4    in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! @{keyword "|"})) end
     7.5  
     7.6  val _ =
     7.7 -  Outer_Syntax.local_theory @{command_spec "fixrec"} "define recursive functions (HOLCF)"
     7.8 +  Outer_Syntax.local_theory @{command_keyword fixrec} "define recursive functions (HOLCF)"
     7.9      (Parse.fixes -- (Parse.where_ |-- Parse.!!! alt_specs')
    7.10        >> (fn (fixes, specs) => add_fixrec_cmd fixes specs))
    7.11  
     8.1 --- a/src/HOL/Import/import_data.ML	Mon Apr 06 16:30:44 2015 +0200
     8.2 +++ b/src/HOL/Import/import_data.ML	Mon Apr 06 17:06:48 2015 +0200
     8.3 @@ -117,13 +117,13 @@
     8.4    "declare a type_definition theorem as a map for an imported type with abs and rep")
     8.5  
     8.6  val _ =
     8.7 -  Outer_Syntax.command @{command_spec "import_type_map"}
     8.8 +  Outer_Syntax.command @{command_keyword import_type_map}
     8.9      "map external type name to existing Isabelle/HOL type name"
    8.10      ((Parse.name --| @{keyword ":"}) -- Parse.type_const >>
    8.11        (fn (ty_name1, ty_name2) => Toplevel.theory (add_typ_map_cmd ty_name1 ty_name2)))
    8.12  
    8.13  val _ =
    8.14 -  Outer_Syntax.command @{command_spec "import_const_map"}
    8.15 +  Outer_Syntax.command @{command_keyword import_const_map}
    8.16      "map external const name to existing Isabelle/HOL const name"
    8.17      ((Parse.name --| @{keyword ":"}) -- Parse.const >>
    8.18        (fn (cname1, cname2) => Toplevel.theory (add_const_map_cmd cname1 cname2)))
     9.1 --- a/src/HOL/Import/import_rule.ML	Mon Apr 06 16:30:44 2015 +0200
     9.2 +++ b/src/HOL/Import/import_rule.ML	Mon Apr 06 17:06:48 2015 +0200
     9.3 @@ -444,7 +444,7 @@
     9.4  fun process_file path thy =
     9.5    (thy, init_state) |> File.fold_lines process_line path |> fst
     9.6  
     9.7 -val _ = Outer_Syntax.command @{command_spec "import_file"}
     9.8 +val _ = Outer_Syntax.command @{command_keyword import_file}
     9.9    "import a recorded proof file"
    9.10    (Parse.path >> (fn name => Toplevel.theory (fn thy => process_file (Path.explode name) thy)))
    9.11  
    10.1 --- a/src/HOL/Library/Old_SMT/old_smt_config.ML	Mon Apr 06 16:30:44 2015 +0200
    10.2 +++ b/src/HOL/Library/Old_SMT/old_smt_config.ML	Mon Apr 06 17:06:48 2015 +0200
    10.3 @@ -246,7 +246,7 @@
    10.4    end
    10.5  
    10.6  val _ =
    10.7 -  Outer_Syntax.command @{command_spec "old_smt_status"}
    10.8 +  Outer_Syntax.command @{command_keyword old_smt_status}
    10.9      "show the available SMT solvers, the currently selected SMT solver, \
   10.10      \and the values of SMT configuration options"
   10.11      (Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of)))
    11.1 --- a/src/HOL/Library/bnf_axiomatization.ML	Mon Apr 06 16:30:44 2015 +0200
    11.2 +++ b/src/HOL/Library/bnf_axiomatization.ML	Mon Apr 06 17:06:48 2015 +0200
    11.3 @@ -118,7 +118,7 @@
    11.4    parse_witTs -- Parse.opt_mixfix -- parse_map_rel_bindings;
    11.5  
    11.6  val _ =
    11.7 -  Outer_Syntax.local_theory @{command_spec "bnf_axiomatization"} "bnf declaration"
    11.8 +  Outer_Syntax.local_theory @{command_keyword bnf_axiomatization} "bnf declaration"
    11.9      (parse_bnf_axiomatization >> 
   11.10        (fn (((((plugins, bsTs), b), witTs), mx), (mapb, relb)) =>
   11.11           bnf_axiomatization_cmd plugins bsTs b mx mapb relb witTs #> snd));
    12.1 --- a/src/HOL/Library/code_test.ML	Mon Apr 06 16:30:44 2015 +0200
    12.2 +++ b/src/HOL/Library/code_test.ML	Mon Apr 06 17:06:48 2015 +0200
    12.3 @@ -567,7 +567,7 @@
    12.4  val test_codeP = Scan.repeat1 Parse.prop -- (@{keyword "in"} |-- Scan.repeat1 Parse.name)
    12.5  
    12.6  val _ = 
    12.7 -  Outer_Syntax.command @{command_spec "test_code"}
    12.8 +  Outer_Syntax.command @{command_keyword test_code}
    12.9      "compile test cases to target languages, execute them and report results"
   12.10        (test_codeP >> (fn (raw_ts, targets) => Toplevel.keep (test_code_cmd raw_ts targets)))
   12.11  
    13.1 --- a/src/HOL/Library/refute.ML	Mon Apr 06 16:30:44 2015 +0200
    13.2 +++ b/src/HOL/Library/refute.ML	Mon Apr 06 17:06:48 2015 +0200
    13.3 @@ -2965,7 +2965,7 @@
    13.4  (* 'refute' command *)
    13.5  
    13.6  val _ =
    13.7 -  Outer_Syntax.command @{command_spec "refute"}
    13.8 +  Outer_Syntax.command @{command_keyword refute}
    13.9      "try to find a model that refutes a given subgoal"
   13.10      (scan_parms -- Scan.optional Parse.nat 1 >>
   13.11        (fn (parms, i) =>
   13.12 @@ -2980,7 +2980,7 @@
   13.13  (* 'refute_params' command *)
   13.14  
   13.15  val _ =
   13.16 -  Outer_Syntax.command @{command_spec "refute_params"}
   13.17 +  Outer_Syntax.command @{command_keyword refute_params}
   13.18      "show/store default parameters for the 'refute' command"
   13.19      (scan_parms >> (fn parms =>
   13.20        Toplevel.theory (fn thy =>
    14.1 --- a/src/HOL/Library/simps_case_conv.ML	Mon Apr 06 16:30:44 2015 +0200
    14.2 +++ b/src/HOL/Library/simps_case_conv.ML	Mon Apr 06 17:06:48 2015 +0200
    14.3 @@ -219,7 +219,7 @@
    14.4    end
    14.5  
    14.6  val _ =
    14.7 -  Outer_Syntax.local_theory @{command_spec "case_of_simps"}
    14.8 +  Outer_Syntax.local_theory @{command_keyword case_of_simps}
    14.9      "turn a list of equations into a case expression"
   14.10      (Parse_Spec.opt_thm_name ":"  -- Parse.xthms1 >> case_of_simps_cmd)
   14.11  
   14.12 @@ -227,7 +227,7 @@
   14.13    Parse.xthms1 --| @{keyword ")"}
   14.14  
   14.15  val _ =
   14.16 -  Outer_Syntax.local_theory @{command_spec "simps_of_case"}
   14.17 +  Outer_Syntax.local_theory @{command_keyword simps_of_case}
   14.18      "perform case split on rule"
   14.19      (Parse_Spec.opt_thm_name ":"  -- Parse.xthm --
   14.20        Scan.optional parse_splits [] >> simps_of_case_cmd)
    15.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Mon Apr 06 16:30:44 2015 +0200
    15.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Mon Apr 06 17:06:48 2015 +0200
    15.3 @@ -1018,7 +1018,7 @@
    15.4  (* syntax und parsing *)
    15.5  
    15.6  val _ =
    15.7 -  Outer_Syntax.command @{command_spec "atom_decl"} "declare new kinds of atoms"
    15.8 +  Outer_Syntax.command @{command_keyword atom_decl} "declare new kinds of atoms"
    15.9      (Scan.repeat1 Parse.name >> (Toplevel.theory o create_nom_typedecls));
   15.10  
   15.11  end;
    16.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Mon Apr 06 16:30:44 2015 +0200
    16.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Mon Apr 06 17:06:48 2015 +0200
    16.3 @@ -2074,7 +2074,7 @@
    16.4  val nominal_datatype_cmd = gen_nominal_datatype Old_Datatype.read_specs;
    16.5  
    16.6  val _ =
    16.7 -  Outer_Syntax.command @{command_spec "nominal_datatype"} "define nominal datatypes"
    16.8 +  Outer_Syntax.command @{command_keyword nominal_datatype} "define nominal datatypes"
    16.9      (Parse.and_list1 Old_Datatype.spec_cmd >>
   16.10        (Toplevel.theory o nominal_datatype_cmd Old_Datatype_Aux.default_config));
   16.11  
    17.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Mon Apr 06 16:30:44 2015 +0200
    17.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Mon Apr 06 17:06:48 2015 +0200
    17.3 @@ -671,14 +671,14 @@
    17.4  (* outer syntax *)
    17.5  
    17.6  val _ =
    17.7 -  Outer_Syntax.local_theory_to_proof @{command_spec "nominal_inductive"}
    17.8 +  Outer_Syntax.local_theory_to_proof @{command_keyword nominal_inductive}
    17.9      "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes"
   17.10      (Parse.xname -- Scan.optional (@{keyword "avoids"} |-- Parse.and_list1 (Parse.name --
   17.11        (@{keyword ":"} |-- Scan.repeat1 Parse.name))) [] >> (fn (name, avoids) =>
   17.12          prove_strong_ind name avoids));
   17.13  
   17.14  val _ =
   17.15 -  Outer_Syntax.local_theory @{command_spec "equivariance"}
   17.16 +  Outer_Syntax.local_theory @{command_keyword equivariance}
   17.17      "prove equivariance for inductive predicate involving nominal datatypes"
   17.18      (Parse.xname -- Scan.optional (@{keyword "["} |-- Parse.list1 Parse.name --| @{keyword "]"}) [] >>
   17.19        (fn (name, atoms) => prove_eqvt name atoms));
    18.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Mon Apr 06 16:30:44 2015 +0200
    18.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Mon Apr 06 17:06:48 2015 +0200
    18.3 @@ -483,7 +483,7 @@
    18.4  (* outer syntax *)
    18.5  
    18.6  val _ =
    18.7 -  Outer_Syntax.local_theory_to_proof @{command_spec "nominal_inductive2"}
    18.8 +  Outer_Syntax.local_theory_to_proof @{command_keyword nominal_inductive2}
    18.9      "prove strong induction theorem for inductive predicate involving nominal datatypes"
   18.10      (Parse.xname -- 
   18.11       Scan.option (@{keyword "("} |-- Parse.!!! (Parse.name --| @{keyword ")"})) --
    19.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Mon Apr 06 16:30:44 2015 +0200
    19.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Mon Apr 06 17:06:48 2015 +0200
    19.3 @@ -403,7 +403,7 @@
    19.4    Scan.optional (@{keyword "("} |-- Parse.!!! (parser2 --| @{keyword ")"})) (NONE, NONE);
    19.5  
    19.6  val _ =
    19.7 -  Outer_Syntax.local_theory_to_proof @{command_spec "nominal_primrec"}
    19.8 +  Outer_Syntax.local_theory_to_proof @{command_keyword nominal_primrec}
    19.9      "define primitive recursive functions on nominal datatypes"
   19.10      (options -- Parse.fixes -- Parse.for_fixes -- Parse_Spec.where_alt_specs
   19.11        >> (fn ((((invs, fctxt), fixes), params), specs) =>
    20.1 --- a/src/HOL/Orderings.thy	Mon Apr 06 16:30:44 2015 +0200
    20.2 +++ b/src/HOL/Orderings.thy	Mon Apr 06 17:06:48 2015 +0200
    20.3 @@ -439,7 +439,7 @@
    20.4    end;
    20.5  
    20.6  val _ =
    20.7 -  Outer_Syntax.command @{command_spec "print_orders"}
    20.8 +  Outer_Syntax.command @{command_keyword print_orders}
    20.9      "print order structures available to transitivity reasoner"
   20.10      (Scan.succeed (Toplevel.unknown_context o
   20.11        Toplevel.keep (print_structures o Toplevel.context_of)));
    21.1 --- a/src/HOL/SMT_Examples/boogie.ML	Mon Apr 06 16:30:44 2015 +0200
    21.2 +++ b/src/HOL/SMT_Examples/boogie.ML	Mon Apr 06 17:06:48 2015 +0200
    21.3 @@ -266,7 +266,7 @@
    21.4  (* Isar command *)
    21.5  
    21.6  val _ =
    21.7 -  Outer_Syntax.command @{command_spec "boogie_file"}
    21.8 +  Outer_Syntax.command @{command_keyword boogie_file}
    21.9      "prove verification condition from .b2i file"
   21.10      (Resources.provide_parse_files "boogie_file" >> (fn files =>
   21.11        Toplevel.theory (fn thy =>
    22.1 --- a/src/HOL/SPARK/Tools/spark_commands.ML	Mon Apr 06 16:30:44 2015 +0200
    22.2 +++ b/src/HOL/SPARK/Tools/spark_commands.ML	Mon Apr 06 17:06:48 2015 +0200
    22.3 @@ -92,13 +92,13 @@
    22.4    end;
    22.5  
    22.6  val _ =
    22.7 -  Outer_Syntax.command @{command_spec "spark_open_vcg"}
    22.8 +  Outer_Syntax.command @{command_keyword spark_open_vcg}
    22.9      "open a new SPARK environment and load a SPARK-generated .vcg file"
   22.10      (Resources.provide_parse_files "spark_open_vcg" -- Parse.parname
   22.11        >> (Toplevel.theory o spark_open Fdl_Lexer.vcg_header));
   22.12  
   22.13  val _ =
   22.14 -  Outer_Syntax.command @{command_spec "spark_open"}
   22.15 +  Outer_Syntax.command @{command_keyword spark_open}
   22.16      "open a new SPARK environment and load a SPARK-generated .siv file"
   22.17      (Resources.provide_parse_files "spark_open" -- Parse.parname
   22.18        >> (Toplevel.theory o spark_open Fdl_Lexer.siv_header));
   22.19 @@ -107,13 +107,13 @@
   22.20    (Args.parens (Parse.list1 Parse.name) --| Args.colon -- Parse.name);
   22.21  
   22.22  val _ =
   22.23 -  Outer_Syntax.command @{command_spec "spark_proof_functions"}
   22.24 +  Outer_Syntax.command @{command_keyword spark_proof_functions}
   22.25      "associate SPARK proof functions with terms"
   22.26      (Scan.repeat1 (Parse.name -- (pfun_type --| Args.$$$ "=" -- Parse.term)) >>
   22.27        (Toplevel.theory o fold add_proof_fun_cmd));
   22.28  
   22.29  val _ =
   22.30 -  Outer_Syntax.command @{command_spec "spark_types"}
   22.31 +  Outer_Syntax.command @{command_keyword spark_types}
   22.32      "associate SPARK types with types"
   22.33      (Scan.repeat1 (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.typ --
   22.34         Scan.optional (Args.parens (Parse.list1
   22.35 @@ -121,12 +121,12 @@
   22.36         (Toplevel.theory o fold add_spark_type_cmd));
   22.37  
   22.38  val _ =
   22.39 -  Outer_Syntax.local_theory_to_proof @{command_spec "spark_vc"}
   22.40 +  Outer_Syntax.local_theory_to_proof @{command_keyword spark_vc}
   22.41      "enter into proof mode for a specific verification condition"
   22.42      (Parse.name >> prove_vc);
   22.43  
   22.44  val _ =
   22.45 -  Outer_Syntax.command @{command_spec "spark_status"}
   22.46 +  Outer_Syntax.command @{command_keyword spark_status}
   22.47      "show the name and state of all loaded verification conditions"
   22.48      (Scan.optional
   22.49         (Args.parens
   22.50 @@ -136,7 +136,7 @@
   22.51          Toplevel.keep (fn state => show_status (Toplevel.theory_of state) args)))
   22.52  
   22.53  val _ =
   22.54 -  Outer_Syntax.command @{command_spec "spark_end"}
   22.55 +  Outer_Syntax.command @{command_keyword spark_end}
   22.56      "close the current SPARK environment"
   22.57      (Scan.optional (@{keyword "("} |-- Parse.!!!
   22.58           (Parse.reserved "incomplete" --| @{keyword ")"}) >> K true) false >>
    23.1 --- a/src/HOL/Statespace/state_space.ML	Mon Apr 06 16:30:44 2015 +0200
    23.2 +++ b/src/HOL/Statespace/state_space.ML	Mon Apr 06 17:06:48 2015 +0200
    23.3 @@ -650,7 +650,7 @@
    23.4          (plus1_unless comp parent --
    23.5            Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 comp)) [])));
    23.6  val _ =
    23.7 -  Outer_Syntax.command @{command_spec "statespace"} "define state-space as locale context"
    23.8 +  Outer_Syntax.command @{command_keyword statespace} "define state-space as locale context"
    23.9      (statespace_decl >> (fn ((args, name), (parents, comps)) =>
   23.10        Toplevel.theory (define_statespace args name parents comps)));
   23.11  
    24.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Mon Apr 06 16:30:44 2015 +0200
    24.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Mon Apr 06 17:06:48 2015 +0200
    24.3 @@ -912,7 +912,7 @@
    24.4    in TPTP_Data.map (cons ((prob_name, result))) thy' end
    24.5  
    24.6  val _ =
    24.7 -  Outer_Syntax.command @{command_spec "import_tptp"} "import TPTP problem"
    24.8 +  Outer_Syntax.command @{command_keyword import_tptp} "import TPTP problem"
    24.9      (Parse.path >> (fn name =>
   24.10        Toplevel.theory (fn thy =>
   24.11          let val path = Path.explode name
    25.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Mon Apr 06 16:30:44 2015 +0200
    25.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Mon Apr 06 17:06:48 2015 +0200
    25.3 @@ -1854,7 +1854,7 @@
    25.4  
    25.5  (*This has been disabled since it requires a hook to be specified to use "import_thm"
    25.6  val _ =
    25.7 -  Outer_Syntax.command @{command_spec "import_leo2_proof"} "import TPTP proof"
    25.8 +  Outer_Syntax.command @{command_keyword import_leo2_proof} "import TPTP proof"
    25.9      (Parse.path >> (fn name =>
   25.10        Toplevel.theory (fn thy =>
   25.11         let val path = Path.explode name
    26.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Mon Apr 06 16:30:44 2015 +0200
    26.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Apr 06 17:06:48 2015 +0200
    26.3 @@ -1615,12 +1615,12 @@
    26.4    end;
    26.5  
    26.6  val _ =
    26.7 -  Outer_Syntax.command @{command_spec "print_bnfs"}
    26.8 +  Outer_Syntax.command @{command_keyword print_bnfs}
    26.9      "print all bounded natural functors"
   26.10      (Scan.succeed (Toplevel.keep (print_bnfs o Toplevel.context_of)));
   26.11  
   26.12  val _ =
   26.13 -  Outer_Syntax.local_theory_to_proof @{command_spec "bnf"}
   26.14 +  Outer_Syntax.local_theory_to_proof @{command_keyword bnf}
   26.15      "register a type as a bounded natural functor"
   26.16      (parse_opt_binding_colon -- Parse.typ --|
   26.17         (Parse.reserved "map" -- @{keyword ":"}) -- Parse.term --
    27.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Apr 06 16:30:44 2015 +0200
    27.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Apr 06 17:06:48 2015 +0200
    27.3 @@ -2019,7 +2019,7 @@
    27.4              val fake_T = qsoty (unfreeze_fp X);
    27.5              val fake_T_backdrop = qsoty (unfreeze_fp X_backdrop);
    27.6              fun register_hint () =
    27.7 -              "\nUse the " ^ quote (#1 @{command_spec "bnf"}) ^ " command to register " ^
    27.8 +              "\nUse the " ^ quote (#1 @{command_keyword bnf}) ^ " command to register " ^
    27.9                quote bad_tc ^ " as a bounded natural functor to allow nested (co)recursion through \
   27.10                \it";
   27.11            in
    28.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Apr 06 16:30:44 2015 +0200
    28.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Apr 06 17:06:48 2015 +0200
    28.3 @@ -2555,7 +2555,7 @@
    28.4    end;
    28.5  
    28.6  val _ =
    28.7 -  Outer_Syntax.local_theory @{command_spec "codatatype"} "define coinductive datatypes"
    28.8 +  Outer_Syntax.local_theory @{command_keyword codatatype} "define coinductive datatypes"
    28.9      (parse_co_datatype_cmd Greatest_FP construct_gfp);
   28.10  
   28.11  val _ = Theory.setup (fp_antiquote_setup @{binding codatatype});
    29.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Apr 06 16:30:44 2015 +0200
    29.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Apr 06 17:06:48 2015 +0200
    29.3 @@ -112,8 +112,8 @@
    29.4  fun unexpected_corec_call ctxt eqns t =
    29.5    error_at ctxt eqns ("Unexpected corecursive call in " ^ quote (Syntax.string_of_term ctxt t));
    29.6  fun use_primcorecursive () =
    29.7 -  error ("\"auto\" failed (try " ^ quote (#1 @{command_spec "primcorecursive"}) ^ " instead of " ^
    29.8 -    quote (#1 @{command_spec "primcorec"}) ^ ")");
    29.9 +  error ("\"auto\" failed (try " ^ quote (#1 @{command_keyword primcorecursive}) ^ " instead of " ^
   29.10 +    quote (#1 @{command_keyword primcorec}) ^ ")");
   29.11  
   29.12  datatype corec_option =
   29.13    Plugins_Option of Proof.context -> Plugin_Name.filter |
   29.14 @@ -1551,13 +1551,13 @@
   29.15  val where_alt_props_of_parser = Parse.where_ |-- Parse.!!! (Parse.enum1 "|"
   29.16    ((Parse.prop >> pair Attrib.empty_binding) -- Scan.option (Parse.reserved "of" |-- Parse.const)));
   29.17  
   29.18 -val _ = Outer_Syntax.local_theory_to_proof @{command_spec "primcorecursive"}
   29.19 +val _ = Outer_Syntax.local_theory_to_proof @{command_keyword primcorecursive}
   29.20    "define primitive corecursive functions"
   29.21    ((Scan.optional (@{keyword "("} |--
   29.22        Parse.!!! (Parse.list1 corec_option_parser) --| @{keyword ")"}) []) --
   29.23      (Parse.fixes -- where_alt_props_of_parser) >> uncurry add_primcorecursive_cmd);
   29.24  
   29.25 -val _ = Outer_Syntax.local_theory @{command_spec "primcorec"}
   29.26 +val _ = Outer_Syntax.local_theory @{command_keyword primcorec}
   29.27    "define primitive corecursive functions"
   29.28    ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser)
   29.29        --| @{keyword ")"}) []) --
    30.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Apr 06 16:30:44 2015 +0200
    30.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Apr 06 17:06:48 2015 +0200
    30.3 @@ -1842,7 +1842,7 @@
    30.4    end;
    30.5  
    30.6  val _ =
    30.7 -  Outer_Syntax.local_theory @{command_spec "datatype"} "define inductive datatypes"
    30.8 +  Outer_Syntax.local_theory @{command_keyword datatype} "define inductive datatypes"
    30.9      (parse_co_datatype_cmd Least_FP construct_lfp);
   30.10  
   30.11  val _ = Theory.setup (fp_antiquote_setup @{binding datatype});
    31.1 --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Apr 06 16:30:44 2015 +0200
    31.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Apr 06 17:06:48 2015 +0200
    31.3 @@ -539,7 +539,7 @@
    31.4    BNF_LFP_Rec_Sugar.add_primrec_simple;
    31.5  
    31.6  val _ =
    31.7 -  Outer_Syntax.local_theory @{command_spec "datatype_compat"}
    31.8 +  Outer_Syntax.local_theory @{command_keyword datatype_compat}
    31.9      "register datatypes as old-style datatypes and derive old-style properties"
   31.10      (Scan.repeat1 Parse.type_const >> datatype_compat_cmd);
   31.11  
    32.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Apr 06 16:30:44 2015 +0200
    32.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Apr 06 17:06:48 2015 +0200
    32.3 @@ -669,7 +669,7 @@
    32.4     || Parse.reserved "nonexhaustive" >> K Nonexhaustive_Option
    32.5     || Parse.reserved "transfer" >> K Transfer_Option);
    32.6  
    32.7 -val _ = Outer_Syntax.local_theory @{command_spec "primrec"}
    32.8 +val _ = Outer_Syntax.local_theory @{command_keyword primrec}
    32.9    "define primitive recursive functions"
   32.10    ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 rec_option_parser)
   32.11        --| @{keyword ")"}) []) --
    33.1 --- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Mon Apr 06 16:30:44 2015 +0200
    33.2 +++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Mon Apr 06 17:06:48 2015 +0200
    33.3 @@ -630,7 +630,7 @@
    33.4    end;
    33.5  
    33.6  val _ =
    33.7 -  Outer_Syntax.command @{command_spec "print_case_translations"}
    33.8 +  Outer_Syntax.command @{command_keyword print_case_translations}
    33.9      "print registered case combinators and constructors"
   33.10      (Scan.succeed (Toplevel.keep (print_case_translations o Toplevel.context_of)))
   33.11  
    34.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Apr 06 16:30:44 2015 +0200
    34.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Apr 06 17:06:48 2015 +0200
    34.3 @@ -1143,7 +1143,7 @@
    34.4  val parse_sel_default_eqs = Scan.optional (@{keyword "where"} |-- Parse.enum1 "|" Parse.prop) [];
    34.5  
    34.6  val _ =
    34.7 -  Outer_Syntax.local_theory_to_proof @{command_spec "free_constructors"}
    34.8 +  Outer_Syntax.local_theory_to_proof @{command_keyword free_constructors}
    34.9      "register an existing freely generated type's constructors"
   34.10      (parse_ctr_options -- Parse.binding --| @{keyword "for"} -- parse_ctr_specs
   34.11         -- parse_sel_default_eqs
    35.1 --- a/src/HOL/Tools/Function/fun.ML	Mon Apr 06 16:30:44 2015 +0200
    35.2 +++ b/src/HOL/Tools/Function/fun.ML	Mon Apr 06 17:06:48 2015 +0200
    35.3 @@ -172,7 +172,7 @@
    35.4  
    35.5  
    35.6  val _ =
    35.7 -  Outer_Syntax.local_theory' @{command_spec "fun"}
    35.8 +  Outer_Syntax.local_theory' @{command_keyword fun}
    35.9      "define general recursive functions (short version)"
   35.10      (function_parser fun_config
   35.11        >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config))
    36.1 --- a/src/HOL/Tools/Function/fun_cases.ML	Mon Apr 06 16:30:44 2015 +0200
    36.2 +++ b/src/HOL/Tools/Function/fun_cases.ML	Mon Apr 06 17:06:48 2015 +0200
    36.3 @@ -54,7 +54,7 @@
    36.4  val fun_cases_cmd = gen_fun_cases Attrib.check_src Syntax.read_prop;
    36.5  
    36.6  val _ =
    36.7 -  Outer_Syntax.local_theory @{command_spec "fun_cases"}
    36.8 +  Outer_Syntax.local_theory @{command_keyword fun_cases}
    36.9      "create simplified instances of elimination rules for function equations"
   36.10      (Parse.and_list1 Parse_Spec.specs >> (snd oo fun_cases_cmd));
   36.11  
    37.1 --- a/src/HOL/Tools/Function/function.ML	Mon Apr 06 16:30:44 2015 +0200
    37.2 +++ b/src/HOL/Tools/Function/function.ML	Mon Apr 06 17:06:48 2015 +0200
    37.3 @@ -286,13 +286,13 @@
    37.4  (* outer syntax *)
    37.5  
    37.6  val _ =
    37.7 -  Outer_Syntax.local_theory_to_proof' @{command_spec "function"}
    37.8 +  Outer_Syntax.local_theory_to_proof' @{command_keyword function}
    37.9      "define general recursive functions"
   37.10      (function_parser default_config
   37.11        >> (fn ((config, fixes), statements) => function_cmd fixes statements config))
   37.12  
   37.13  val _ =
   37.14 -  Outer_Syntax.local_theory_to_proof @{command_spec "termination"}
   37.15 +  Outer_Syntax.local_theory_to_proof @{command_keyword termination}
   37.16      "prove termination of a recursive function"
   37.17      (Scan.option Parse.term >> termination_cmd)
   37.18  
    38.1 --- a/src/HOL/Tools/Function/partial_function.ML	Mon Apr 06 16:30:44 2015 +0200
    38.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Mon Apr 06 17:06:48 2015 +0200
    38.3 @@ -309,7 +309,7 @@
    38.4  val mode = @{keyword "("} |-- Parse.xname --| @{keyword ")"};
    38.5  
    38.6  val _ =
    38.7 -  Outer_Syntax.local_theory @{command_spec "partial_function"} "define partial function"
    38.8 +  Outer_Syntax.local_theory @{command_keyword partial_function} "define partial function"
    38.9      ((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.spec)))
   38.10        >> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec));
   38.11  
    39.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Mon Apr 06 16:30:44 2015 +0200
    39.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Mon Apr 06 17:06:48 2015 +0200
    39.3 @@ -700,7 +700,7 @@
    39.4      --| @{keyword "is"} -- Parse.term -- 
    39.5        Scan.optional (@{keyword "parametric"} |-- Parse.!!! Parse.xthms1) []) >> Parse.triple1
    39.6  val _ =
    39.7 -  Outer_Syntax.local_theory_to_proof @{command_spec "lift_definition"}
    39.8 +  Outer_Syntax.local_theory_to_proof @{command_keyword lift_definition}
    39.9      "definition for constants over the quotient type"
   39.10        (liftdef_parser >> lift_def_cmd_with_err_handling)
   39.11  
    40.1 --- a/src/HOL/Tools/Lifting/lifting_info.ML	Mon Apr 06 16:30:44 2015 +0200
    40.2 +++ b/src/HOL/Tools/Lifting/lifting_info.ML	Mon Apr 06 17:06:48 2015 +0200
    40.3 @@ -533,11 +533,11 @@
    40.4  (* outer syntax commands *)
    40.5  
    40.6  val _ =
    40.7 -  Outer_Syntax.command @{command_spec "print_quot_maps"} "print quotient map functions"
    40.8 +  Outer_Syntax.command @{command_keyword print_quot_maps} "print quotient map functions"
    40.9      (Scan.succeed (Toplevel.keep (print_quot_maps o Toplevel.context_of)))
   40.10  
   40.11  val _ =
   40.12 -  Outer_Syntax.command @{command_spec "print_quotients"} "print quotients"
   40.13 +  Outer_Syntax.command @{command_keyword print_quotients} "print quotients"
   40.14      (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
   40.15  
   40.16  end
    41.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Apr 06 16:30:44 2015 +0200
    41.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Apr 06 17:06:48 2015 +0200
    41.3 @@ -787,7 +787,7 @@
    41.4    end
    41.5  
    41.6  val _ = 
    41.7 -  Outer_Syntax.local_theory @{command_spec "setup_lifting"}
    41.8 +  Outer_Syntax.local_theory @{command_keyword setup_lifting}
    41.9      "setup lifting infrastructure" 
   41.10        (Parse.xthm -- Scan.option Parse.xthm 
   41.11        -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm) >> 
   41.12 @@ -998,7 +998,7 @@
   41.13  
   41.14  
   41.15  val _ =
   41.16 -  Outer_Syntax.local_theory @{command_spec "lifting_forget"} 
   41.17 +  Outer_Syntax.local_theory @{command_keyword lifting_forget} 
   41.18      "unsetup Lifting and Transfer for the given lifting bundle"
   41.19      (Parse.position Parse.xname >> (lifting_forget_cmd))
   41.20  
   41.21 @@ -1027,7 +1027,7 @@
   41.22    update_transfer_rules (pointer_of_bundle_name bundle_name lthy) lthy
   41.23  
   41.24  val _ =
   41.25 -  Outer_Syntax.local_theory @{command_spec "lifting_update"}
   41.26 +  Outer_Syntax.local_theory @{command_keyword lifting_update}
   41.27      "add newly introduced transfer rules to a bundle storing the state of Lifting and Transfer"
   41.28      (Parse.position Parse.xname >> lifting_update_cmd)
   41.29  
    42.1 --- a/src/HOL/Tools/Nitpick/nitpick_commands.ML	Mon Apr 06 16:30:44 2015 +0200
    42.2 +++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML	Mon Apr 06 17:06:48 2015 +0200
    42.3 @@ -374,7 +374,7 @@
    42.4                                        |> sort_strings |> cat_lines)))))
    42.5  
    42.6  val _ =
    42.7 -  Outer_Syntax.command @{command_spec "nitpick"}
    42.8 +  Outer_Syntax.command @{command_keyword nitpick}
    42.9      "try to find a counterexample for a given subgoal using Nitpick"
   42.10      (parse_params -- Scan.optional Parse.nat 1 >> (fn (params, i) =>
   42.11        Toplevel.unknown_proof o
   42.12 @@ -383,7 +383,7 @@
   42.13            (Toplevel.proof_of state)))))
   42.14  
   42.15  val _ =
   42.16 -  Outer_Syntax.command @{command_spec "nitpick_params"}
   42.17 +  Outer_Syntax.command @{command_keyword nitpick_params}
   42.18      "set and display the default parameters for Nitpick"
   42.19      (parse_params #>> nitpick_params_trans)
   42.20  
    43.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Mon Apr 06 16:30:44 2015 +0200
    43.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Mon Apr 06 17:06:48 2015 +0200
    43.3 @@ -788,7 +788,7 @@
    43.4    >> (fn (((vs, t), mx), cons) => ((t, vs, mx), map Parse.triple1 cons));
    43.5  
    43.6  val _ =
    43.7 -  Outer_Syntax.command @{command_spec "old_datatype"} "define old-style inductive datatypes"
    43.8 +  Outer_Syntax.command @{command_keyword old_datatype} "define old-style inductive datatypes"
    43.9      (Parse.and_list1 spec_cmd
   43.10        >> (Toplevel.theory o (snd oo add_datatype_cmd Old_Datatype_Aux.default_config)));
   43.11  
    44.1 --- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Mon Apr 06 16:30:44 2015 +0200
    44.2 +++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Mon Apr 06 17:06:48 2015 +0200
    44.3 @@ -680,7 +680,7 @@
    44.4  (* outer syntax *)
    44.5  
    44.6  val _ =
    44.7 -  Outer_Syntax.command @{command_spec "old_rep_datatype"}
    44.8 +  Outer_Syntax.command @{command_keyword old_rep_datatype}
    44.9      "register existing types as old-style datatypes"
   44.10      (Scan.repeat1 Parse.term >> (fn ts =>
   44.11        Toplevel.theory_to_proof (rep_datatype_cmd Old_Datatype_Aux.default_config (K I) ts)));
    45.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Apr 06 16:30:44 2015 +0200
    45.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Apr 06 17:06:48 2015 +0200
    45.3 @@ -1033,7 +1033,7 @@
    45.4    Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []
    45.5  
    45.6  val _ =
    45.7 -  Outer_Syntax.command @{command_spec "values_prolog"}
    45.8 +  Outer_Syntax.command @{command_keyword values_prolog}
    45.9      "enumerate and print comprehensions"
   45.10      (opt_print_modes -- Scan.optional (Parse.nat >> SOME) NONE -- Parse.term
   45.11       >> (fn ((print_modes, soln), t) => Toplevel.keep (values_cmd print_modes soln t)))
    46.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon Apr 06 16:30:44 2015 +0200
    46.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon Apr 06 17:06:48 2015 +0200
    46.3 @@ -278,12 +278,12 @@
    46.4  (* code_pred command and values command *)
    46.5  
    46.6  val _ =
    46.7 -  Outer_Syntax.local_theory_to_proof @{command_spec "code_pred"}
    46.8 +  Outer_Syntax.local_theory_to_proof @{command_keyword code_pred}
    46.9      "prove equations for predicate specified by intro/elim rules"
   46.10      (opt_expected_modes -- opt_modes -- scan_options -- Parse.term >> code_pred_cmd)
   46.11  
   46.12  val _ =
   46.13 -  Outer_Syntax.command @{command_spec "values"}
   46.14 +  Outer_Syntax.command @{command_keyword values}
   46.15      "enumerate and print comprehensions"
   46.16      (opt_print_modes -- opt_param_modes -- value_options -- Scan.optional Parse.nat ~1 -- Parse.term
   46.17        >> (fn ((((print_modes, param_modes), options), k), t) => Toplevel.keep
    47.1 --- a/src/HOL/Tools/Quickcheck/abstract_generators.ML	Mon Apr 06 16:30:44 2015 +0200
    47.2 +++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML	Mon Apr 06 17:06:48 2015 +0200
    47.3 @@ -67,7 +67,7 @@
    47.4      Syntax.read_term
    47.5    
    47.6  val _ =
    47.7 -  Outer_Syntax.command @{command_spec "quickcheck_generator"}
    47.8 +  Outer_Syntax.command @{command_keyword quickcheck_generator}
    47.9      "define quickcheck generators for abstract types"
   47.10      ((Parse.type_const --
   47.11        Scan.option (Args.$$$ "predicate" |-- @{keyword ":"} |-- Parse.term)) --
    48.1 --- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Mon Apr 06 16:30:44 2015 +0200
    48.2 +++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Mon Apr 06 17:06:48 2015 +0200
    48.3 @@ -111,7 +111,7 @@
    48.4  end
    48.5  
    48.6  val _ =
    48.7 -  Outer_Syntax.command @{command_spec "find_unused_assms"}
    48.8 +  Outer_Syntax.command @{command_keyword find_unused_assms}
    48.9      "find theorems with (potentially) superfluous assumptions"
   48.10      (Scan.option Parse.name >> (fn name =>
   48.11        Toplevel.keep (fn state => print_unused_assms (Toplevel.context_of state) name)))
    49.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Mon Apr 06 16:30:44 2015 +0200
    49.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Mon Apr 06 17:06:48 2015 +0200
    49.3 @@ -213,7 +213,7 @@
    49.4      Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| @{keyword "is"} -- Parse.term))
    49.5  
    49.6  val _ =
    49.7 -  Outer_Syntax.local_theory_to_proof @{command_spec "quotient_definition"}
    49.8 +  Outer_Syntax.local_theory_to_proof @{command_keyword quotient_definition}
    49.9      "definition for constants over the quotient type"
   49.10        (quotdef_parser >> quotient_def_cmd)
   49.11  
    50.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Mon Apr 06 16:30:44 2015 +0200
    50.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Mon Apr 06 17:06:48 2015 +0200
    50.3 @@ -229,15 +229,15 @@
    50.4  (* outer syntax commands *)
    50.5  
    50.6  val _ =
    50.7 -  Outer_Syntax.command @{command_spec "print_quotmapsQ3"} "print quotient map functions"
    50.8 +  Outer_Syntax.command @{command_keyword print_quotmapsQ3} "print quotient map functions"
    50.9      (Scan.succeed (Toplevel.keep (print_quotmaps o Toplevel.context_of)))
   50.10  
   50.11  val _ =
   50.12 -  Outer_Syntax.command @{command_spec "print_quotientsQ3"} "print quotients"
   50.13 +  Outer_Syntax.command @{command_keyword print_quotientsQ3} "print quotients"
   50.14      (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
   50.15  
   50.16  val _ =
   50.17 -  Outer_Syntax.command @{command_spec "print_quotconsts"} "print quotient constants"
   50.18 +  Outer_Syntax.command @{command_keyword print_quotconsts} "print quotient constants"
   50.19      (Scan.succeed (Toplevel.keep (print_quotconsts o Toplevel.context_of)))
   50.20  
   50.21  end;
    51.1 --- a/src/HOL/Tools/Quotient/quotient_type.ML	Mon Apr 06 16:30:44 2015 +0200
    51.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML	Mon Apr 06 17:06:48 2015 +0200
    51.3 @@ -342,7 +342,7 @@
    51.4            -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm)
    51.5  
    51.6  val _ =
    51.7 -  Outer_Syntax.local_theory_to_proof @{command_spec "quotient_type"}
    51.8 +  Outer_Syntax.local_theory_to_proof @{command_keyword quotient_type}
    51.9      "quotient type definitions (require equivalence proofs)"
   51.10        (quotspec_parser >> quotient_type_cmd)
   51.11  
    52.1 --- a/src/HOL/Tools/SMT/smt_config.ML	Mon Apr 06 16:30:44 2015 +0200
    52.2 +++ b/src/HOL/Tools/SMT/smt_config.ML	Mon Apr 06 17:06:48 2015 +0200
    52.3 @@ -257,7 +257,7 @@
    52.4    end
    52.5  
    52.6  val _ =
    52.7 -  Outer_Syntax.command @{command_spec "smt_status"}
    52.8 +  Outer_Syntax.command @{command_keyword smt_status}
    52.9      "show the available SMT solvers, the currently selected SMT solver, \
   52.10      \and the values of SMT configuration options"
   52.11      (Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of)))
    53.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Apr 06 16:30:44 2015 +0200
    53.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Apr 06 17:06:48 2015 +0200
    53.3 @@ -387,12 +387,12 @@
    53.4      no_fact_override
    53.5  
    53.6  val _ =
    53.7 -  Outer_Syntax.command @{command_spec "sledgehammer"}
    53.8 +  Outer_Syntax.command @{command_keyword sledgehammer}
    53.9      "search for first-order proof using automatic theorem provers"
   53.10      ((Scan.optional Parse.name runN -- parse_params
   53.11        -- parse_fact_override -- Scan.option Parse.nat) #>> sledgehammer_trans)
   53.12  val _ =
   53.13 -  Outer_Syntax.command @{command_spec "sledgehammer_params"}
   53.14 +  Outer_Syntax.command @{command_keyword sledgehammer_params}
   53.15      "set and display the default parameters for Sledgehammer"
   53.16      (parse_params #>> sledgehammer_params_trans)
   53.17  
    54.1 --- a/src/HOL/Tools/choice_specification.ML	Mon Apr 06 16:30:44 2015 +0200
    54.2 +++ b/src/HOL/Tools/choice_specification.ML	Mon Apr 06 17:06:48 2015 +0200
    54.3 @@ -198,7 +198,7 @@
    54.4  val opt_overloaded = Parse.opt_keyword "overloaded"
    54.5  
    54.6  val _ =
    54.7 -  Outer_Syntax.command @{command_spec "specification"} "define constants by specification"
    54.8 +  Outer_Syntax.command @{command_keyword specification} "define constants by specification"
    54.9      (@{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} --
   54.10        Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop)
   54.11        >> (fn (cos, alt_props) => Toplevel.theory_to_proof (process_spec cos alt_props)))
    55.1 --- a/src/HOL/Tools/functor.ML	Mon Apr 06 16:30:44 2015 +0200
    55.2 +++ b/src/HOL/Tools/functor.ML	Mon Apr 06 17:06:48 2015 +0200
    55.3 @@ -273,7 +273,7 @@
    55.4  val functor_cmd = gen_functor Syntax.read_term;
    55.5  
    55.6  val _ =
    55.7 -  Outer_Syntax.local_theory_to_proof @{command_spec "functor"}
    55.8 +  Outer_Syntax.local_theory_to_proof @{command_keyword functor}
    55.9      "register operations managing the functorial structure of a type"
   55.10      (Scan.option (Parse.name --| @{keyword ":"}) -- Parse.term
   55.11        >> (fn (prfx, t) => functor_cmd prfx t));
    56.1 --- a/src/HOL/Tools/inductive.ML	Mon Apr 06 16:30:44 2015 +0200
    56.2 +++ b/src/HOL/Tools/inductive.ML	Mon Apr 06 17:06:48 2015 +0200
    56.3 @@ -1171,25 +1171,25 @@
    56.4  val ind_decl = gen_ind_decl add_ind_def;
    56.5  
    56.6  val _ =
    56.7 -  Outer_Syntax.local_theory @{command_spec "inductive"} "define inductive predicates"
    56.8 +  Outer_Syntax.local_theory @{command_keyword inductive} "define inductive predicates"
    56.9      (ind_decl false);
   56.10  
   56.11  val _ =
   56.12 -  Outer_Syntax.local_theory @{command_spec "coinductive"} "define coinductive predicates"
   56.13 +  Outer_Syntax.local_theory @{command_keyword coinductive} "define coinductive predicates"
   56.14      (ind_decl true);
   56.15  
   56.16  val _ =
   56.17 -  Outer_Syntax.local_theory @{command_spec "inductive_cases"}
   56.18 +  Outer_Syntax.local_theory @{command_keyword inductive_cases}
   56.19      "create simplified instances of elimination rules"
   56.20      (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
   56.21  
   56.22  val _ =
   56.23 -  Outer_Syntax.local_theory @{command_spec "inductive_simps"}
   56.24 +  Outer_Syntax.local_theory @{command_keyword inductive_simps}
   56.25      "create simplification rules for inductive predicates"
   56.26      (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_simps));
   56.27  
   56.28  val _ =
   56.29 -  Outer_Syntax.command @{command_spec "print_inductives"}
   56.30 +  Outer_Syntax.command @{command_keyword print_inductives}
   56.31      "print (co)inductive definitions and monotonicity rules"
   56.32      (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
   56.33        Toplevel.keep (print_inductives b o Toplevel.context_of)));
    57.1 --- a/src/HOL/Tools/inductive_set.ML	Mon Apr 06 16:30:44 2015 +0200
    57.2 +++ b/src/HOL/Tools/inductive_set.ML	Mon Apr 06 17:06:48 2015 +0200
    57.3 @@ -568,11 +568,11 @@
    57.4  val ind_set_decl = Inductive.gen_ind_decl add_ind_set_def;
    57.5  
    57.6  val _ =
    57.7 -  Outer_Syntax.local_theory @{command_spec "inductive_set"} "define inductive sets"
    57.8 +  Outer_Syntax.local_theory @{command_keyword inductive_set} "define inductive sets"
    57.9      (ind_set_decl false);
   57.10  
   57.11  val _ =
   57.12 -  Outer_Syntax.local_theory @{command_spec "coinductive_set"} "define coinductive sets"
   57.13 +  Outer_Syntax.local_theory @{command_keyword coinductive_set} "define coinductive sets"
   57.14      (ind_set_decl true);
   57.15  
   57.16  end;
    58.1 --- a/src/HOL/Tools/recdef.ML	Mon Apr 06 16:30:44 2015 +0200
    58.2 +++ b/src/HOL/Tools/recdef.ML	Mon Apr 06 17:06:48 2015 +0200
    58.3 @@ -298,7 +298,7 @@
    58.4    >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map Parse.triple_swap eqs) src);
    58.5  
    58.6  val _ =
    58.7 -  Outer_Syntax.command @{command_spec "recdef"} "define general recursive functions (obsolete TFL)"
    58.8 +  Outer_Syntax.command @{command_keyword recdef} "define general recursive functions (obsolete TFL)"
    58.9      (recdef_decl >> Toplevel.theory);
   58.10  
   58.11  
   58.12 @@ -309,12 +309,12 @@
   58.13    >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
   58.14  
   58.15  val _ =
   58.16 -  Outer_Syntax.command @{command_spec "defer_recdef"}
   58.17 +  Outer_Syntax.command @{command_keyword defer_recdef}
   58.18      "defer general recursive functions (obsolete TFL)"
   58.19      (defer_recdef_decl >> Toplevel.theory);
   58.20  
   58.21  val _ =
   58.22 -  Outer_Syntax.local_theory_to_proof' @{command_spec "recdef_tc"}
   58.23 +  Outer_Syntax.local_theory_to_proof' @{command_keyword recdef_tc}
   58.24      "recommence proof of termination condition (obsolete TFL)"
   58.25      ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.xname --
   58.26          Scan.option (@{keyword "("} |-- Parse.nat --| @{keyword ")"})
    59.1 --- a/src/HOL/Tools/record.ML	Mon Apr 06 16:30:44 2015 +0200
    59.2 +++ b/src/HOL/Tools/record.ML	Mon Apr 06 17:06:48 2015 +0200
    59.3 @@ -2329,7 +2329,7 @@
    59.4  (* outer syntax *)
    59.5  
    59.6  val _ =
    59.7 -  Outer_Syntax.command @{command_spec "record"} "define extensible record"
    59.8 +  Outer_Syntax.command @{command_keyword record} "define extensible record"
    59.9      (Parse.type_args_constrained -- Parse.binding --
   59.10        (@{keyword "="} |-- Scan.option (Parse.typ --| @{keyword "+"}) --
   59.11          Scan.repeat1 Parse.const_binding)
    60.1 --- a/src/HOL/Tools/try0.ML	Mon Apr 06 16:30:44 2015 +0200
    60.2 +++ b/src/HOL/Tools/try0.ML	Mon Apr 06 17:06:48 2015 +0200
    60.3 @@ -177,7 +177,7 @@
    60.4     || Scan.repeat parse_attr >> (fn quad => fold merge_attrs quad ([], [], [], []))) x;
    60.5  
    60.6  val _ =
    60.7 -  Outer_Syntax.command @{command_spec "try0"} "try a combination of proof methods"
    60.8 +  Outer_Syntax.command @{command_keyword try0} "try a combination of proof methods"
    60.9      (Scan.optional parse_attrs ([], [], [], []) #>> try0_trans);
   60.10  
   60.11  fun try_try0 auto = generic_try0 (if auto then Auto_Try else Try) NONE ([], [], [], []);
    61.1 --- a/src/HOL/Tools/typedef.ML	Mon Apr 06 16:30:44 2015 +0200
    61.2 +++ b/src/HOL/Tools/typedef.ML	Mon Apr 06 17:06:48 2015 +0200
    61.3 @@ -281,7 +281,7 @@
    61.4  (** outer syntax **)
    61.5  
    61.6  val _ =
    61.7 -  Outer_Syntax.local_theory_to_proof @{command_spec "typedef"}
    61.8 +  Outer_Syntax.local_theory_to_proof @{command_keyword typedef}
    61.9      "HOL type definition (requires non-emptiness proof)"
   61.10      (Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
   61.11        (@{keyword "="} |-- Parse.term) --
    62.1 --- a/src/HOL/Tools/value.ML	Mon Apr 06 16:30:44 2015 +0200
    62.2 +++ b/src/HOL/Tools/value.ML	Mon Apr 06 17:06:48 2015 +0200
    62.3 @@ -70,7 +70,7 @@
    62.4    Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"})
    62.5    
    62.6  val _ =
    62.7 -  Outer_Syntax.command @{command_spec "value"} "evaluate and print term"
    62.8 +  Outer_Syntax.command @{command_keyword value} "evaluate and print term"
    62.9      (opt_evaluator -- opt_modes -- Parse.term
   62.10        >> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t)));
   62.11  
    63.1 --- a/src/HOL/ex/Cartouche_Examples.thy	Mon Apr 06 16:30:44 2015 +0200
    63.2 +++ b/src/HOL/ex/Cartouche_Examples.thy	Mon Apr 06 17:06:48 2015 +0200
    63.3 @@ -40,7 +40,7 @@
    63.4  subsection \<open>Outer syntax: cartouche within command syntax\<close>
    63.5  
    63.6  ML \<open>
    63.7 -  Outer_Syntax.command @{command_spec "cartouche"} ""
    63.8 +  Outer_Syntax.command @{command_keyword cartouche} ""
    63.9      (Parse.cartouche >> (fn s =>
   63.10        Toplevel.imperative (fn () => writeln s)))
   63.11  \<close>
   63.12 @@ -116,7 +116,7 @@
   63.13  subsubsection \<open>Term cartouche and regular quotes\<close>
   63.14  
   63.15  ML \<open>
   63.16 -  Outer_Syntax.command @{command_spec "term_cartouche"} ""
   63.17 +  Outer_Syntax.command @{command_keyword term_cartouche} ""
   63.18      (Parse.inner_syntax Parse.cartouche >> (fn s =>
   63.19        Toplevel.keep (fn state =>
   63.20          let
   63.21 @@ -178,7 +178,7 @@
   63.22  
   63.23  ML \<open>
   63.24    Outer_Syntax.command
   63.25 -    @{command_spec "text_cartouche"} ""
   63.26 +    @{command_keyword text_cartouche} ""
   63.27      (Parse.opt_target -- Parse.input Parse.cartouche >> Thy_Output.document_command)
   63.28  \<close>
   63.29  
    64.1 --- a/src/HOL/ex/Commands.thy	Mon Apr 06 16:30:44 2015 +0200
    64.2 +++ b/src/HOL/ex/Commands.thy	Mon Apr 06 17:06:48 2015 +0200
    64.3 @@ -15,7 +15,7 @@
    64.4  subsection \<open>Diagnostic command: no state change\<close>
    64.5  
    64.6  ML \<open>
    64.7 -  Outer_Syntax.command @{command_spec "print_test"} "print term test"
    64.8 +  Outer_Syntax.command @{command_keyword print_test} "print term test"
    64.9      (Parse.term >> (fn s => Toplevel.keep (fn st =>
   64.10        let
   64.11          val ctxt = Toplevel.context_of st;
   64.12 @@ -30,7 +30,7 @@
   64.13  subsection \<open>Old-style global theory declaration\<close>
   64.14  
   64.15  ML \<open>
   64.16 -  Outer_Syntax.command @{command_spec "global_test"} "test constant declaration"
   64.17 +  Outer_Syntax.command @{command_keyword global_test} "test constant declaration"
   64.18      (Parse.binding >> (fn b => Toplevel.theory (fn thy =>
   64.19        let
   64.20          val thy' = Sign.add_consts [(b, @{typ 'a}, NoSyn)] thy;
   64.21 @@ -45,7 +45,7 @@
   64.22  subsection \<open>Local theory specification\<close>
   64.23  
   64.24  ML \<open>
   64.25 -  Outer_Syntax.local_theory @{command_spec "local_test"} "test local definition"
   64.26 +  Outer_Syntax.local_theory @{command_keyword local_test} "test local definition"
   64.27      (Parse.binding -- (@{keyword "="} |-- Parse.term) >> (fn (b, s) => fn lthy =>
   64.28        let
   64.29          val t = Syntax.read_term lthy s;
    65.1 --- a/src/Provers/classical.ML	Mon Apr 06 16:30:44 2015 +0200
    65.2 +++ b/src/Provers/classical.ML	Mon Apr 06 17:06:48 2015 +0200
    65.3 @@ -974,7 +974,7 @@
    65.4  (** outer syntax **)
    65.5  
    65.6  val _ =
    65.7 -  Outer_Syntax.command @{command_spec "print_claset"} "print context of Classical Reasoner"
    65.8 +  Outer_Syntax.command @{command_keyword print_claset} "print context of Classical Reasoner"
    65.9      (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_claset o Toplevel.context_of)));
   65.10  
   65.11  end;
    66.1 --- a/src/Pure/Isar/calculation.ML	Mon Apr 06 16:30:44 2015 +0200
    66.2 +++ b/src/Pure/Isar/calculation.ML	Mon Apr 06 17:06:48 2015 +0200
    66.3 @@ -211,25 +211,25 @@
    66.4    Scan.option (@{keyword "("} |-- Parse.!!! ((Parse.xthms1 --| @{keyword ")"})));
    66.5  
    66.6  val _ =
    66.7 -  Outer_Syntax.command @{command_spec "also"} "combine calculation and current facts"
    66.8 +  Outer_Syntax.command @{command_keyword also} "combine calculation and current facts"
    66.9      (calc_args >> (Toplevel.proofs' o also_cmd));
   66.10  
   66.11  val _ =
   66.12 -  Outer_Syntax.command @{command_spec "finally"}
   66.13 +  Outer_Syntax.command @{command_keyword finally}
   66.14      "combine calculation and current facts, exhibit result"
   66.15      (calc_args >> (Toplevel.proofs' o finally_cmd));
   66.16  
   66.17  val _ =
   66.18 -  Outer_Syntax.command @{command_spec "moreover"} "augment calculation by current facts"
   66.19 +  Outer_Syntax.command @{command_keyword moreover} "augment calculation by current facts"
   66.20      (Scan.succeed (Toplevel.proof' moreover));
   66.21  
   66.22  val _ =
   66.23 -  Outer_Syntax.command @{command_spec "ultimately"}
   66.24 +  Outer_Syntax.command @{command_keyword ultimately}
   66.25      "augment calculation by current facts, exhibit result"
   66.26      (Scan.succeed (Toplevel.proof' ultimately));
   66.27  
   66.28  val _ =
   66.29 -  Outer_Syntax.command @{command_spec "print_trans_rules"} "print transitivity rules"
   66.30 +  Outer_Syntax.command @{command_keyword print_trans_rules} "print transitivity rules"
   66.31      (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_rules o Toplevel.context_of)));
   66.32  
   66.33  end;
    67.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Apr 06 16:30:44 2015 +0200
    67.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Apr 06 17:06:48 2015 +0200
    67.3 @@ -12,7 +12,7 @@
    67.4  (* sorts *)
    67.5  
    67.6  val _ =
    67.7 -  Outer_Syntax.local_theory @{command_spec "default_sort"}
    67.8 +  Outer_Syntax.local_theory @{command_keyword default_sort}
    67.9      "declare default sort for explicit type variables"
   67.10      (Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy));
   67.11  
   67.12 @@ -20,18 +20,18 @@
   67.13  (* types *)
   67.14  
   67.15  val _ =
   67.16 -  Outer_Syntax.local_theory @{command_spec "typedecl"} "type declaration"
   67.17 +  Outer_Syntax.local_theory @{command_keyword typedecl} "type declaration"
   67.18      (Parse.type_args -- Parse.binding -- Parse.opt_mixfix
   67.19        >> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd));
   67.20  
   67.21  val _ =
   67.22 -  Outer_Syntax.local_theory @{command_spec "type_synonym"} "declare type abbreviation"
   67.23 +  Outer_Syntax.local_theory @{command_keyword type_synonym} "declare type abbreviation"
   67.24      (Parse.type_args -- Parse.binding --
   67.25        (@{keyword "="} |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'))
   67.26        >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs));
   67.27  
   67.28  val _ =
   67.29 -  Outer_Syntax.command @{command_spec "nonterminal"}
   67.30 +  Outer_Syntax.command @{command_keyword nonterminal}
   67.31      "declare syntactic type constructors (grammar nonterminal symbols)"
   67.32      (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global));
   67.33  
   67.34 @@ -39,11 +39,11 @@
   67.35  (* consts and syntax *)
   67.36  
   67.37  val _ =
   67.38 -  Outer_Syntax.command @{command_spec "judgment"} "declare object-logic judgment"
   67.39 +  Outer_Syntax.command @{command_keyword judgment} "declare object-logic judgment"
   67.40      (Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
   67.41  
   67.42  val _ =
   67.43 -  Outer_Syntax.command @{command_spec "consts"} "declare constants"
   67.44 +  Outer_Syntax.command @{command_keyword consts} "declare constants"
   67.45      (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts_cmd));
   67.46  
   67.47  val mode_spec =
   67.48 @@ -54,12 +54,12 @@
   67.49    Scan.optional (@{keyword "("} |-- Parse.!!! (mode_spec --| @{keyword ")"})) Syntax.mode_default;
   67.50  
   67.51  val _ =
   67.52 -  Outer_Syntax.command @{command_spec "syntax"} "add raw syntax clauses"
   67.53 +  Outer_Syntax.command @{command_keyword syntax} "add raw syntax clauses"
   67.54      (opt_mode -- Scan.repeat1 Parse.const_decl
   67.55        >> (Toplevel.theory o uncurry Sign.add_syntax_cmd));
   67.56  
   67.57  val _ =
   67.58 -  Outer_Syntax.command @{command_spec "no_syntax"} "delete raw syntax clauses"
   67.59 +  Outer_Syntax.command @{command_keyword no_syntax} "delete raw syntax clauses"
   67.60      (opt_mode -- Scan.repeat1 Parse.const_decl
   67.61        >> (Toplevel.theory o uncurry Sign.del_syntax_cmd));
   67.62  
   67.63 @@ -81,11 +81,11 @@
   67.64      >> (fn (left, (arr, right)) => arr (left, right));
   67.65  
   67.66  val _ =
   67.67 -  Outer_Syntax.command @{command_spec "translations"} "add syntax translation rules"
   67.68 +  Outer_Syntax.command @{command_keyword translations} "add syntax translation rules"
   67.69      (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations));
   67.70  
   67.71  val _ =
   67.72 -  Outer_Syntax.command @{command_spec "no_translations"} "delete syntax translation rules"
   67.73 +  Outer_Syntax.command @{command_keyword no_translations} "delete syntax translation rules"
   67.74      (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations));
   67.75  
   67.76  
   67.77 @@ -98,7 +98,7 @@
   67.78        @{keyword "overloaded"} >> K (false, true)) --| @{keyword ")"})) (false, false);
   67.79  
   67.80  val _ =
   67.81 -  Outer_Syntax.command @{command_spec "defs"} "define constants"
   67.82 +  Outer_Syntax.command @{command_keyword defs} "define constants"
   67.83      (opt_unchecked_overloaded --
   67.84        Scan.repeat1 (Parse_Spec.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y)))
   67.85        >> (Toplevel.theory o Isar_Cmd.add_defs));
   67.86 @@ -107,34 +107,34 @@
   67.87  (* constant definitions and abbreviations *)
   67.88  
   67.89  val _ =
   67.90 -  Outer_Syntax.local_theory' @{command_spec "definition"} "constant definition"
   67.91 +  Outer_Syntax.local_theory' @{command_keyword definition} "constant definition"
   67.92      (Parse_Spec.constdef >> (fn args => #2 oo Specification.definition_cmd args));
   67.93  
   67.94  val _ =
   67.95 -  Outer_Syntax.local_theory' @{command_spec "abbreviation"} "constant abbreviation"
   67.96 +  Outer_Syntax.local_theory' @{command_keyword abbreviation} "constant abbreviation"
   67.97      (opt_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
   67.98        >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
   67.99  
  67.100  val _ =
  67.101 -  Outer_Syntax.local_theory @{command_spec "type_notation"}
  67.102 +  Outer_Syntax.local_theory @{command_keyword type_notation}
  67.103      "add concrete syntax for type constructors"
  67.104      (opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
  67.105        >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
  67.106  
  67.107  val _ =
  67.108 -  Outer_Syntax.local_theory @{command_spec "no_type_notation"}
  67.109 +  Outer_Syntax.local_theory @{command_keyword no_type_notation}
  67.110      "delete concrete syntax for type constructors"
  67.111      (opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
  67.112        >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
  67.113  
  67.114  val _ =
  67.115 -  Outer_Syntax.local_theory @{command_spec "notation"}
  67.116 +  Outer_Syntax.local_theory @{command_keyword notation}
  67.117      "add concrete syntax for constants / fixed variables"
  67.118      (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
  67.119        >> (fn (mode, args) => Specification.notation_cmd true mode args));
  67.120  
  67.121  val _ =
  67.122 -  Outer_Syntax.local_theory @{command_spec "no_notation"}
  67.123 +  Outer_Syntax.local_theory @{command_keyword no_notation}
  67.124      "delete concrete syntax for constants / fixed variables"
  67.125      (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
  67.126        >> (fn (mode, args) => Specification.notation_cmd false mode args));
  67.127 @@ -143,7 +143,7 @@
  67.128  (* constant specifications *)
  67.129  
  67.130  val _ =
  67.131 -  Outer_Syntax.command @{command_spec "axiomatization"} "axiomatic constant specification"
  67.132 +  Outer_Syntax.command @{command_keyword axiomatization} "axiomatic constant specification"
  67.133      (Scan.optional Parse.fixes [] --
  67.134        Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 Parse_Spec.specs)) []
  67.135        >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));
  67.136 @@ -156,14 +156,14 @@
  67.137      >> (fn (facts, fixes) => #2 oo Specification.theorems_cmd kind facts fixes);
  67.138  
  67.139  val _ =
  67.140 -  Outer_Syntax.local_theory' @{command_spec "theorems"} "define theorems"
  67.141 +  Outer_Syntax.local_theory' @{command_keyword theorems} "define theorems"
  67.142      (theorems Thm.theoremK);
  67.143  
  67.144  val _ =
  67.145 -  Outer_Syntax.local_theory' @{command_spec "lemmas"} "define lemmas" (theorems Thm.lemmaK);
  67.146 +  Outer_Syntax.local_theory' @{command_keyword lemmas} "define lemmas" (theorems Thm.lemmaK);
  67.147  
  67.148  val _ =
  67.149 -  Outer_Syntax.local_theory' @{command_spec "declare"} "declare theorems"
  67.150 +  Outer_Syntax.local_theory' @{command_keyword declare} "declare theorems"
  67.151      (Parse.and_list1 Parse.xthms1 -- Parse.for_fixes
  67.152        >> (fn (facts, fixes) =>
  67.153            #2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
  67.154 @@ -183,19 +183,19 @@
  67.155  in
  67.156  
  67.157  val _ =
  67.158 -  hide_names @{command_spec "hide_class"} "classes" Sign.hide_class Parse.class
  67.159 +  hide_names @{command_keyword hide_class} "classes" Sign.hide_class Parse.class
  67.160      Proof_Context.read_class;
  67.161  
  67.162  val _ =
  67.163 -  hide_names @{command_spec "hide_type"} "types" Sign.hide_type Parse.type_const
  67.164 +  hide_names @{command_keyword hide_type} "types" Sign.hide_type Parse.type_const
  67.165      ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = false});
  67.166  
  67.167  val _ =
  67.168 -  hide_names @{command_spec "hide_const"} "constants" Sign.hide_const Parse.const
  67.169 +  hide_names @{command_keyword hide_const} "constants" Sign.hide_const Parse.const
  67.170      ((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false});
  67.171  
  67.172  val _ =
  67.173 -  hide_names @{command_spec "hide_fact"} "facts" Global_Theory.hide_fact
  67.174 +  hide_names @{command_keyword hide_fact} "facts" Global_Theory.hide_fact
  67.175      (Parse.position Parse.xname) (Global_Theory.check_fact o Proof_Context.theory_of);
  67.176  
  67.177  end;
  67.178 @@ -204,7 +204,7 @@
  67.179  (* use ML text *)
  67.180  
  67.181  val _ =
  67.182 -  Outer_Syntax.command @{command_spec "SML_file"} "read and evaluate Standard ML file"
  67.183 +  Outer_Syntax.command @{command_keyword SML_file} "read and evaluate Standard ML file"
  67.184      (Resources.provide_parse_files "SML_file" >> (fn files => Toplevel.theory (fn thy =>
  67.185          let
  67.186            val ([{lines, pos, ...}], thy') = files thy;
  67.187 @@ -216,7 +216,7 @@
  67.188          end)));
  67.189  
  67.190  val _ =
  67.191 -  Outer_Syntax.command @{command_spec "SML_export"} "evaluate SML within Isabelle/ML environment"
  67.192 +  Outer_Syntax.command @{command_keyword SML_export} "evaluate SML within Isabelle/ML environment"
  67.193      (Parse.ML_source >> (fn source =>
  67.194        let val flags = {SML = true, exchange = true, redirect = false, verbose = true} in
  67.195          Toplevel.theory
  67.196 @@ -224,7 +224,7 @@
  67.197        end));
  67.198  
  67.199  val _ =
  67.200 -  Outer_Syntax.command @{command_spec "SML_import"} "evaluate Isabelle/ML within SML environment"
  67.201 +  Outer_Syntax.command @{command_keyword SML_import} "evaluate Isabelle/ML within SML environment"
  67.202      (Parse.ML_source >> (fn source =>
  67.203        let val flags = {SML = false, exchange = true, redirect = false, verbose = true} in
  67.204          Toplevel.generic_theory
  67.205 @@ -233,7 +233,7 @@
  67.206        end));
  67.207  
  67.208  val _ =
  67.209 -  Outer_Syntax.command @{command_spec "ML"} "ML text within theory or local theory"
  67.210 +  Outer_Syntax.command @{command_keyword ML} "ML text within theory or local theory"
  67.211      (Parse.ML_source >> (fn source =>
  67.212        Toplevel.generic_theory
  67.213          (ML_Context.exec (fn () =>
  67.214 @@ -241,7 +241,7 @@
  67.215            Local_Theory.propagate_ml_env)));
  67.216  
  67.217  val _ =
  67.218 -  Outer_Syntax.command @{command_spec "ML_prf"} "ML text within proof"
  67.219 +  Outer_Syntax.command @{command_keyword ML_prf} "ML text within proof"
  67.220      (Parse.ML_source >> (fn source =>
  67.221        Toplevel.proof (Proof.map_context (Context.proof_map
  67.222          (ML_Context.exec (fn () =>
  67.223 @@ -249,45 +249,45 @@
  67.224            Proof.propagate_ml_env)));
  67.225  
  67.226  val _ =
  67.227 -  Outer_Syntax.command @{command_spec "ML_val"} "diagnostic ML text"
  67.228 +  Outer_Syntax.command @{command_keyword ML_val} "diagnostic ML text"
  67.229      (Parse.ML_source >> Isar_Cmd.ml_diag true);
  67.230  
  67.231  val _ =
  67.232 -  Outer_Syntax.command @{command_spec "ML_command"} "diagnostic ML text (silent)"
  67.233 +  Outer_Syntax.command @{command_keyword ML_command} "diagnostic ML text (silent)"
  67.234      (Parse.ML_source >> Isar_Cmd.ml_diag false);
  67.235  
  67.236  val _ =
  67.237 -  Outer_Syntax.command @{command_spec "setup"} "ML setup for global theory"
  67.238 +  Outer_Syntax.command @{command_keyword setup} "ML setup for global theory"
  67.239      (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.setup));
  67.240  
  67.241  val _ =
  67.242 -  Outer_Syntax.local_theory @{command_spec "local_setup"} "ML setup for local theory"
  67.243 +  Outer_Syntax.local_theory @{command_keyword local_setup} "ML setup for local theory"
  67.244      (Parse.ML_source >> Isar_Cmd.local_setup);
  67.245  
  67.246  val _ =
  67.247 -  Outer_Syntax.local_theory @{command_spec "attribute_setup"} "define attribute in ML"
  67.248 +  Outer_Syntax.local_theory @{command_keyword attribute_setup} "define attribute in ML"
  67.249      (Parse.position Parse.name --
  67.250          Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
  67.251        >> (fn (name, (txt, cmt)) => Attrib.attribute_setup name txt cmt));
  67.252  
  67.253  val _ =
  67.254 -  Outer_Syntax.local_theory @{command_spec "method_setup"} "define proof method in ML"
  67.255 +  Outer_Syntax.local_theory @{command_keyword method_setup} "define proof method in ML"
  67.256      (Parse.position Parse.name --
  67.257          Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
  67.258        >> (fn (name, (txt, cmt)) => Method.method_setup name txt cmt));
  67.259  
  67.260  val _ =
  67.261 -  Outer_Syntax.local_theory @{command_spec "declaration"} "generic ML declaration"
  67.262 +  Outer_Syntax.local_theory @{command_keyword declaration} "generic ML declaration"
  67.263      (Parse.opt_keyword "pervasive" -- Parse.ML_source
  67.264        >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = false, pervasive = pervasive} txt));
  67.265  
  67.266  val _ =
  67.267 -  Outer_Syntax.local_theory @{command_spec "syntax_declaration"} "generic ML syntax declaration"
  67.268 +  Outer_Syntax.local_theory @{command_keyword syntax_declaration} "generic ML syntax declaration"
  67.269      (Parse.opt_keyword "pervasive" -- Parse.ML_source
  67.270        >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = true, pervasive = pervasive} txt));
  67.271  
  67.272  val _ =
  67.273 -  Outer_Syntax.local_theory @{command_spec "simproc_setup"} "define simproc in ML"
  67.274 +  Outer_Syntax.local_theory @{command_keyword simproc_setup} "define simproc in ML"
  67.275      (Parse.position Parse.name --
  67.276        (@{keyword "("} |-- Parse.enum1 "|" Parse.term --| @{keyword ")"} --| @{keyword "="}) --
  67.277        Parse.ML_source -- Scan.optional (@{keyword "identifier"} |-- Scan.repeat1 Parse.xname) []
  67.278 @@ -297,27 +297,27 @@
  67.279  (* translation functions *)
  67.280  
  67.281  val _ =
  67.282 -  Outer_Syntax.command @{command_spec "parse_ast_translation"}
  67.283 +  Outer_Syntax.command @{command_keyword parse_ast_translation}
  67.284      "install parse ast translation functions"
  67.285      (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_ast_translation));
  67.286  
  67.287  val _ =
  67.288 -  Outer_Syntax.command @{command_spec "parse_translation"}
  67.289 +  Outer_Syntax.command @{command_keyword parse_translation}
  67.290      "install parse translation functions"
  67.291      (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_translation));
  67.292  
  67.293  val _ =
  67.294 -  Outer_Syntax.command @{command_spec "print_translation"}
  67.295 +  Outer_Syntax.command @{command_keyword print_translation}
  67.296      "install print translation functions"
  67.297      (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_translation));
  67.298  
  67.299  val _ =
  67.300 -  Outer_Syntax.command @{command_spec "typed_print_translation"}
  67.301 +  Outer_Syntax.command @{command_keyword typed_print_translation}
  67.302      "install typed print translation functions"
  67.303      (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.typed_print_translation));
  67.304  
  67.305  val _ =
  67.306 -  Outer_Syntax.command @{command_spec "print_ast_translation"}
  67.307 +  Outer_Syntax.command @{command_keyword print_ast_translation}
  67.308      "install print ast translation functions"
  67.309      (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_ast_translation));
  67.310  
  67.311 @@ -325,7 +325,7 @@
  67.312  (* oracles *)
  67.313  
  67.314  val _ =
  67.315 -  Outer_Syntax.command @{command_spec "oracle"} "declare oracle"
  67.316 +  Outer_Syntax.command @{command_keyword oracle} "declare oracle"
  67.317      (Parse.range Parse.name -- (@{keyword "="} |-- Parse.ML_source) >>
  67.318        (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
  67.319  
  67.320 @@ -333,22 +333,22 @@
  67.321  (* bundled declarations *)
  67.322  
  67.323  val _ =
  67.324 -  Outer_Syntax.local_theory @{command_spec "bundle"} "define bundle of declarations"
  67.325 +  Outer_Syntax.local_theory @{command_keyword bundle} "define bundle of declarations"
  67.326      ((Parse.binding --| @{keyword "="}) -- Parse.xthms1 -- Parse.for_fixes
  67.327        >> (uncurry Bundle.bundle_cmd));
  67.328  
  67.329  val _ =
  67.330 -  Outer_Syntax.command @{command_spec "include"}
  67.331 +  Outer_Syntax.command @{command_keyword include}
  67.332      "include declarations from bundle in proof body"
  67.333      (Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.include_cmd));
  67.334  
  67.335  val _ =
  67.336 -  Outer_Syntax.command @{command_spec "including"}
  67.337 +  Outer_Syntax.command @{command_keyword including}
  67.338      "include declarations from bundle in goal refinement"
  67.339      (Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.including_cmd));
  67.340  
  67.341  val _ =
  67.342 -  Outer_Syntax.command @{command_spec "print_bundles"}
  67.343 +  Outer_Syntax.command @{command_keyword print_bundles}
  67.344      "print bundles of declarations"
  67.345      (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
  67.346        Toplevel.keep (Bundle.print_bundles b o Toplevel.context_of)));
  67.347 @@ -357,7 +357,7 @@
  67.348  (* local theories *)
  67.349  
  67.350  val _ =
  67.351 -  Outer_Syntax.command @{command_spec "context"} "begin local theory context"
  67.352 +  Outer_Syntax.command @{command_keyword context} "begin local theory context"
  67.353      ((Parse.position Parse.xname >> (fn name =>
  67.354          Toplevel.begin_local_theory true (Named_Target.begin name)) ||
  67.355        Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
  67.356 @@ -373,7 +373,7 @@
  67.357    Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
  67.358  
  67.359  val _ =
  67.360 -  Outer_Syntax.command @{command_spec "locale"} "define named specification context"
  67.361 +  Outer_Syntax.command @{command_keyword locale} "define named specification context"
  67.362      (Parse.binding --
  67.363        Scan.optional (@{keyword "="} |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
  67.364        >> (fn ((name, (expr, elems)), begin) =>
  67.365 @@ -381,7 +381,7 @@
  67.366              (Expression.add_locale_cmd name Binding.empty expr elems #> snd)));
  67.367  
  67.368  val _ =
  67.369 -  Outer_Syntax.command @{command_spec "experiment"} "open private specification context"
  67.370 +  Outer_Syntax.command @{command_keyword experiment} "open private specification context"
  67.371      (Scan.repeat Parse_Spec.context_element --| Parse.begin
  67.372        >> (fn elems =>
  67.373            Toplevel.begin_local_theory true (Experiment.experiment_cmd elems #> snd)));
  67.374 @@ -392,7 +392,7 @@
  67.375        (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
  67.376  
  67.377  val _ =
  67.378 -  Outer_Syntax.command @{command_spec "sublocale"}
  67.379 +  Outer_Syntax.command @{command_keyword sublocale}
  67.380      "prove sublocale relation between a locale and a locale expression"
  67.381      ((Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
  67.382        interpretation_args false >> (fn (loc, (expr, equations)) =>
  67.383 @@ -401,13 +401,13 @@
  67.384          Toplevel.local_theory_to_proof NONE NONE (Expression.sublocale_cmd expr equations)));
  67.385  
  67.386  val _ =
  67.387 -  Outer_Syntax.command @{command_spec "interpretation"}
  67.388 +  Outer_Syntax.command @{command_keyword interpretation}
  67.389      "prove interpretation of locale expression in local theory"
  67.390      (interpretation_args true >> (fn (expr, equations) =>
  67.391        Toplevel.local_theory_to_proof NONE NONE (Expression.interpretation_cmd expr equations)));
  67.392  
  67.393  val _ =
  67.394 -  Outer_Syntax.command @{command_spec "interpret"}
  67.395 +  Outer_Syntax.command @{command_keyword interpret}
  67.396      "prove interpretation of locale expression in proof context"
  67.397      (interpretation_args true >> (fn (expr, equations) =>
  67.398        Toplevel.proof' (Expression.interpret_cmd expr equations)));
  67.399 @@ -421,23 +421,23 @@
  67.400    Scan.repeat1 Parse_Spec.context_element >> pair [];
  67.401  
  67.402  val _ =
  67.403 -  Outer_Syntax.command @{command_spec "class"} "define type class"
  67.404 +  Outer_Syntax.command @{command_keyword class} "define type class"
  67.405     (Parse.binding -- Scan.optional (@{keyword "="} |-- class_val) ([], []) -- Parse.opt_begin
  67.406      >> (fn ((name, (supclasses, elems)), begin) =>
  67.407          Toplevel.begin_local_theory begin
  67.408            (Class_Declaration.class_cmd name supclasses elems #> snd)));
  67.409  
  67.410  val _ =
  67.411 -  Outer_Syntax.local_theory_to_proof @{command_spec "subclass"} "prove a subclass relation"
  67.412 +  Outer_Syntax.local_theory_to_proof @{command_keyword subclass} "prove a subclass relation"
  67.413      (Parse.class >> Class_Declaration.subclass_cmd);
  67.414  
  67.415  val _ =
  67.416 -  Outer_Syntax.command @{command_spec "instantiation"} "instantiate and prove type arity"
  67.417 +  Outer_Syntax.command @{command_keyword instantiation} "instantiate and prove type arity"
  67.418     (Parse.multi_arity --| Parse.begin
  67.419       >> (fn arities => Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));
  67.420  
  67.421  val _ =
  67.422 -  Outer_Syntax.command @{command_spec "instance"} "prove type arity or subclass relation"
  67.423 +  Outer_Syntax.command @{command_keyword instance} "prove type arity or subclass relation"
  67.424    ((Parse.class --
  67.425      ((@{keyword "\<subseteq>"} || @{keyword "<"}) |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
  67.426      Parse.multi_arity >> Class.instance_arity_cmd) >> Toplevel.theory_to_proof ||
  67.427 @@ -447,7 +447,7 @@
  67.428  (* arbitrary overloading *)
  67.429  
  67.430  val _ =
  67.431 -  Outer_Syntax.command @{command_spec "overloading"} "overloaded definitions"
  67.432 +  Outer_Syntax.command @{command_keyword overloading} "overloaded definitions"
  67.433     (Scan.repeat1 (Parse.name --| (@{keyword "\<equiv>"} || @{keyword "=="}) -- Parse.term --
  67.434        Scan.optional (@{keyword "("} |-- (@{keyword "unchecked"} >> K false) --| @{keyword ")"}) true
  67.435        >> Parse.triple1) --| Parse.begin
  67.436 @@ -457,7 +457,7 @@
  67.437  (* code generation *)
  67.438  
  67.439  val _ =
  67.440 -  Outer_Syntax.command @{command_spec "code_datatype"}
  67.441 +  Outer_Syntax.command @{command_keyword code_datatype}
  67.442      "define set of code datatype constructors"
  67.443      (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.add_datatype_cmd));
  67.444  
  67.445 @@ -478,32 +478,32 @@
  67.446          ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)
  67.447            kind NONE (K I) a includes elems concl)));
  67.448  
  67.449 -val _ = theorem @{command_spec "theorem"} false Thm.theoremK;
  67.450 -val _ = theorem @{command_spec "lemma"} false Thm.lemmaK;
  67.451 -val _ = theorem @{command_spec "corollary"} false Thm.corollaryK;
  67.452 -val _ = theorem @{command_spec "schematic_theorem"} true Thm.theoremK;
  67.453 -val _ = theorem @{command_spec "schematic_lemma"} true Thm.lemmaK;
  67.454 -val _ = theorem @{command_spec "schematic_corollary"} true Thm.corollaryK;
  67.455 +val _ = theorem @{command_keyword theorem} false Thm.theoremK;
  67.456 +val _ = theorem @{command_keyword lemma} false Thm.lemmaK;
  67.457 +val _ = theorem @{command_keyword corollary} false Thm.corollaryK;
  67.458 +val _ = theorem @{command_keyword schematic_theorem} true Thm.theoremK;
  67.459 +val _ = theorem @{command_keyword schematic_lemma} true Thm.lemmaK;
  67.460 +val _ = theorem @{command_keyword schematic_corollary} true Thm.corollaryK;
  67.461  
  67.462  val _ =
  67.463 -  Outer_Syntax.local_theory_to_proof @{command_spec "notepad"} "begin proof context"
  67.464 +  Outer_Syntax.local_theory_to_proof @{command_keyword notepad} "begin proof context"
  67.465      (Parse.begin >> K Proof.begin_notepad);
  67.466  
  67.467  val _ =
  67.468 -  Outer_Syntax.command @{command_spec "have"} "state local goal"
  67.469 +  Outer_Syntax.command @{command_keyword have} "state local goal"
  67.470      (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.have));
  67.471  
  67.472  val _ =
  67.473 -  Outer_Syntax.command @{command_spec "hence"} "old-style alias of \"then have\""
  67.474 +  Outer_Syntax.command @{command_keyword hence} "old-style alias of \"then have\""
  67.475      (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.hence));
  67.476  
  67.477  val _ =
  67.478 -  Outer_Syntax.command @{command_spec "show"}
  67.479 +  Outer_Syntax.command @{command_keyword show}
  67.480      "state local goal, solving current obligation"
  67.481      (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.show));
  67.482  
  67.483  val _ =
  67.484 -  Outer_Syntax.command @{command_spec "thus"} "old-style alias of  \"then show\""
  67.485 +  Outer_Syntax.command @{command_keyword thus} "old-style alias of  \"then show\""
  67.486      (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.thus));
  67.487  
  67.488  
  67.489 @@ -512,46 +512,46 @@
  67.490  val facts = Parse.and_list1 Parse.xthms1;
  67.491  
  67.492  val _ =
  67.493 -  Outer_Syntax.command @{command_spec "then"} "forward chaining"
  67.494 +  Outer_Syntax.command @{command_keyword then} "forward chaining"
  67.495      (Scan.succeed (Toplevel.proof Proof.chain));
  67.496  
  67.497  val _ =
  67.498 -  Outer_Syntax.command @{command_spec "from"} "forward chaining from given facts"
  67.499 +  Outer_Syntax.command @{command_keyword from} "forward chaining from given facts"
  67.500      (facts >> (Toplevel.proof o Proof.from_thmss_cmd));
  67.501  
  67.502  val _ =
  67.503 -  Outer_Syntax.command @{command_spec "with"} "forward chaining from given and current facts"
  67.504 +  Outer_Syntax.command @{command_keyword with} "forward chaining from given and current facts"
  67.505      (facts >> (Toplevel.proof o Proof.with_thmss_cmd));
  67.506  
  67.507  val _ =
  67.508 -  Outer_Syntax.command @{command_spec "note"} "define facts"
  67.509 +  Outer_Syntax.command @{command_keyword note} "define facts"
  67.510      (Parse_Spec.name_facts >> (Toplevel.proof o Proof.note_thmss_cmd));
  67.511  
  67.512  val _ =
  67.513 -  Outer_Syntax.command @{command_spec "using"} "augment goal facts"
  67.514 +  Outer_Syntax.command @{command_keyword using} "augment goal facts"
  67.515      (facts >> (Toplevel.proof o Proof.using_cmd));
  67.516  
  67.517  val _ =
  67.518 -  Outer_Syntax.command @{command_spec "unfolding"} "unfold definitions in goal and facts"
  67.519 +  Outer_Syntax.command @{command_keyword unfolding} "unfold definitions in goal and facts"
  67.520      (facts >> (Toplevel.proof o Proof.unfolding_cmd));
  67.521  
  67.522  
  67.523  (* proof context *)
  67.524  
  67.525  val _ =
  67.526 -  Outer_Syntax.command @{command_spec "fix"} "fix local variables (Skolem constants)"
  67.527 +  Outer_Syntax.command @{command_keyword fix} "fix local variables (Skolem constants)"
  67.528      (Parse.fixes >> (Toplevel.proof o Proof.fix_cmd));
  67.529  
  67.530  val _ =
  67.531 -  Outer_Syntax.command @{command_spec "assume"} "assume propositions"
  67.532 +  Outer_Syntax.command @{command_keyword assume} "assume propositions"
  67.533      (Parse_Spec.statement >> (Toplevel.proof o Proof.assume_cmd));
  67.534  
  67.535  val _ =
  67.536 -  Outer_Syntax.command @{command_spec "presume"} "assume propositions, to be established later"
  67.537 +  Outer_Syntax.command @{command_keyword presume} "assume propositions, to be established later"
  67.538      (Parse_Spec.statement >> (Toplevel.proof o Proof.presume_cmd));
  67.539  
  67.540  val _ =
  67.541 -  Outer_Syntax.command @{command_spec "def"} "local definition (non-polymorphic)"
  67.542 +  Outer_Syntax.command @{command_keyword def} "local definition (non-polymorphic)"
  67.543      (Parse.and_list1
  67.544        (Parse_Spec.opt_thm_name ":" --
  67.545          ((Parse.binding -- Parse.opt_mixfix) --
  67.546 @@ -559,26 +559,26 @@
  67.547      >> (Toplevel.proof o Proof.def_cmd));
  67.548  
  67.549  val _ =
  67.550 -  Outer_Syntax.command @{command_spec "obtain"} "generalized elimination"
  67.551 +  Outer_Syntax.command @{command_keyword obtain} "generalized elimination"
  67.552      (Parse.parname -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement
  67.553        >> (fn ((x, y), z) => Toplevel.proof' (Obtain.obtain_cmd x y z)));
  67.554  
  67.555  val _ =
  67.556 -  Outer_Syntax.command @{command_spec "guess"} "wild guessing (unstructured)"
  67.557 +  Outer_Syntax.command @{command_keyword guess} "wild guessing (unstructured)"
  67.558      (Scan.optional Parse.fixes [] >> (Toplevel.proof' o Obtain.guess_cmd));
  67.559  
  67.560  val _ =
  67.561 -  Outer_Syntax.command @{command_spec "let"} "bind text variables"
  67.562 +  Outer_Syntax.command @{command_keyword let} "bind text variables"
  67.563      (Parse.and_list1 (Parse.and_list1 Parse.term -- (@{keyword "="} |-- Parse.term))
  67.564        >> (Toplevel.proof o Proof.let_bind_cmd));
  67.565  
  67.566  val _ =
  67.567 -  Outer_Syntax.command @{command_spec "write"} "add concrete syntax for constants / fixed variables"
  67.568 +  Outer_Syntax.command @{command_keyword write} "add concrete syntax for constants / fixed variables"
  67.569      (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
  67.570      >> (fn (mode, args) => Toplevel.proof (Proof.write_cmd mode args)));
  67.571  
  67.572  val _ =
  67.573 -  Outer_Syntax.command @{command_spec "case"} "invoke local context"
  67.574 +  Outer_Syntax.command @{command_keyword case} "invoke local context"
  67.575      ((@{keyword "("} |--
  67.576        Parse.!!! (Parse.position Parse.xname -- Scan.repeat (Parse.maybe Parse.binding)
  67.577          --| @{keyword ")"}) ||
  67.578 @@ -589,74 +589,74 @@
  67.579  (* proof structure *)
  67.580  
  67.581  val _ =
  67.582 -  Outer_Syntax.command @{command_spec "{"} "begin explicit proof block"
  67.583 +  Outer_Syntax.command @{command_keyword "{"} "begin explicit proof block"
  67.584      (Scan.succeed (Toplevel.proof Proof.begin_block));
  67.585  
  67.586  val _ =
  67.587 -  Outer_Syntax.command @{command_spec "}"} "end explicit proof block"
  67.588 +  Outer_Syntax.command @{command_keyword "}"} "end explicit proof block"
  67.589      (Scan.succeed (Toplevel.proof Proof.end_block));
  67.590  
  67.591  val _ =
  67.592 -  Outer_Syntax.command @{command_spec "next"} "enter next proof block"
  67.593 +  Outer_Syntax.command @{command_keyword next} "enter next proof block"
  67.594      (Scan.succeed (Toplevel.proof Proof.next_block));
  67.595  
  67.596  
  67.597  (* end proof *)
  67.598  
  67.599  val _ =
  67.600 -  Outer_Syntax.command @{command_spec "qed"} "conclude proof"
  67.601 +  Outer_Syntax.command @{command_keyword qed} "conclude proof"
  67.602      (Scan.option Method.parse >> (fn m =>
  67.603       (Option.map Method.report m;
  67.604        Isar_Cmd.qed m)));
  67.605  
  67.606  val _ =
  67.607 -  Outer_Syntax.command @{command_spec "by"} "terminal backward proof"
  67.608 +  Outer_Syntax.command @{command_keyword by} "terminal backward proof"
  67.609      (Method.parse -- Scan.option Method.parse >> (fn (m1, m2) =>
  67.610       (Method.report m1;
  67.611        Option.map Method.report m2;
  67.612        Isar_Cmd.terminal_proof (m1, m2))));
  67.613  
  67.614  val _ =
  67.615 -  Outer_Syntax.command @{command_spec ".."} "default proof"
  67.616 +  Outer_Syntax.command @{command_keyword ".."} "default proof"
  67.617      (Scan.succeed Isar_Cmd.default_proof);
  67.618  
  67.619  val _ =
  67.620 -  Outer_Syntax.command @{command_spec "."} "immediate proof"
  67.621 +  Outer_Syntax.command @{command_keyword "."} "immediate proof"
  67.622      (Scan.succeed Isar_Cmd.immediate_proof);
  67.623  
  67.624  val _ =
  67.625 -  Outer_Syntax.command @{command_spec "done"} "done proof"
  67.626 +  Outer_Syntax.command @{command_keyword done} "done proof"
  67.627      (Scan.succeed Isar_Cmd.done_proof);
  67.628  
  67.629  val _ =
  67.630 -  Outer_Syntax.command @{command_spec "sorry"} "skip proof (quick-and-dirty mode only!)"
  67.631 +  Outer_Syntax.command @{command_keyword sorry} "skip proof (quick-and-dirty mode only!)"
  67.632      (Scan.succeed Isar_Cmd.skip_proof);
  67.633  
  67.634  val _ =
  67.635 -  Outer_Syntax.command @{command_spec "oops"} "forget proof"
  67.636 +  Outer_Syntax.command @{command_keyword oops} "forget proof"
  67.637      (Scan.succeed (Toplevel.forget_proof true));
  67.638  
  67.639  
  67.640  (* proof steps *)
  67.641  
  67.642  val _ =
  67.643 -  Outer_Syntax.command @{command_spec "defer"} "shuffle internal proof state"
  67.644 +  Outer_Syntax.command @{command_keyword defer} "shuffle internal proof state"
  67.645      (Scan.optional Parse.nat 1 >> (Toplevel.proof o Proof.defer));
  67.646  
  67.647  val _ =
  67.648 -  Outer_Syntax.command @{command_spec "prefer"} "shuffle internal proof state"
  67.649 +  Outer_Syntax.command @{command_keyword prefer} "shuffle internal proof state"
  67.650      (Parse.nat >> (Toplevel.proof o Proof.prefer));
  67.651  
  67.652  val _ =
  67.653 -  Outer_Syntax.command @{command_spec "apply"} "initial refinement step (unstructured)"
  67.654 +  Outer_Syntax.command @{command_keyword apply} "initial refinement step (unstructured)"
  67.655      (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_results m))));
  67.656  
  67.657  val _ =
  67.658 -  Outer_Syntax.command @{command_spec "apply_end"} "terminal refinement step (unstructured)"
  67.659 +  Outer_Syntax.command @{command_keyword apply_end} "terminal refinement step (unstructured)"
  67.660      (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_end_results m))));
  67.661  
  67.662  val _ =
  67.663 -  Outer_Syntax.command @{command_spec "proof"} "backward proof step"
  67.664 +  Outer_Syntax.command @{command_keyword proof} "backward proof step"
  67.665      (Scan.option Method.parse >> (fn m =>
  67.666        (Option.map Method.report m;
  67.667          Toplevel.actual_proof (Proof_Node.applys (Proof.proof_results m)) o
  67.668 @@ -669,7 +669,7 @@
  67.669    Output.report [Markup.markup Markup.bad "Explicit backtracking"];
  67.670  
  67.671  val _ =
  67.672 -  Outer_Syntax.command @{command_spec "back"} "explicit backtracking of proof command"
  67.673 +  Outer_Syntax.command @{command_keyword back} "explicit backtracking of proof command"
  67.674      (Scan.succeed
  67.675       (Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o
  67.676        Toplevel.skip_proof (fn h => (report_back (); h))));
  67.677 @@ -682,194 +682,194 @@
  67.678    Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
  67.679  
  67.680  val _ =
  67.681 -  Outer_Syntax.command @{command_spec "help"}
  67.682 +  Outer_Syntax.command @{command_keyword help}
  67.683      "retrieve outer syntax commands according to name patterns"
  67.684      (Scan.repeat Parse.name >>
  67.685        (fn pats => Toplevel.keep (fn st => Outer_Syntax.help (Toplevel.theory_of st) pats)));
  67.686  
  67.687  val _ =
  67.688 -  Outer_Syntax.command @{command_spec "print_commands"} "print outer syntax commands"
  67.689 +  Outer_Syntax.command @{command_keyword print_commands} "print outer syntax commands"
  67.690      (Scan.succeed (Toplevel.keep (Outer_Syntax.print_commands o Toplevel.theory_of)));
  67.691  
  67.692  val _ =
  67.693 -  Outer_Syntax.command @{command_spec "print_options"} "print configuration options"
  67.694 +  Outer_Syntax.command @{command_keyword print_options} "print configuration options"
  67.695      (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
  67.696        Toplevel.keep (Attrib.print_options b o Toplevel.context_of)));
  67.697  
  67.698  val _ =
  67.699 -  Outer_Syntax.command @{command_spec "print_context"}
  67.700 +  Outer_Syntax.command @{command_keyword print_context}
  67.701      "print context of local theory target"
  67.702      (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_context)));
  67.703  
  67.704  val _ =
  67.705 -  Outer_Syntax.command @{command_spec "print_theory"}
  67.706 +  Outer_Syntax.command @{command_keyword print_theory}
  67.707      "print logical theory contents"
  67.708      (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
  67.709        Toplevel.keep (Pretty.writeln o Proof_Display.pretty_full_theory b o Toplevel.theory_of)));
  67.710  
  67.711  val _ =
  67.712 -  Outer_Syntax.command @{command_spec "print_syntax"}
  67.713 +  Outer_Syntax.command @{command_keyword print_syntax}
  67.714      "print inner syntax of context"
  67.715      (Scan.succeed (Toplevel.unknown_context o
  67.716        Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
  67.717  
  67.718  val _ =
  67.719 -  Outer_Syntax.command @{command_spec "print_defn_rules"}
  67.720 +  Outer_Syntax.command @{command_keyword print_defn_rules}
  67.721      "print definitional rewrite rules of context"
  67.722      (Scan.succeed (Toplevel.unknown_context o
  67.723        Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of)));
  67.724  
  67.725  val _ =
  67.726 -  Outer_Syntax.command @{command_spec "print_abbrevs"}
  67.727 +  Outer_Syntax.command @{command_keyword print_abbrevs}
  67.728      "print constant abbreviations of context"
  67.729      (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
  67.730        Toplevel.keep (Proof_Context.print_abbrevs b o Toplevel.context_of)));
  67.731  
  67.732  val _ =
  67.733 -  Outer_Syntax.command @{command_spec "print_theorems"}
  67.734 +  Outer_Syntax.command @{command_keyword print_theorems}
  67.735      "print theorems of local theory or proof context"
  67.736      (Parse.opt_bang >> (fn b =>
  67.737        Toplevel.unknown_context o
  67.738        Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b)));
  67.739  
  67.740  val _ =
  67.741 -  Outer_Syntax.command @{command_spec "print_locales"}
  67.742 +  Outer_Syntax.command @{command_keyword print_locales}
  67.743      "print locales of this theory"
  67.744      (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
  67.745        Toplevel.keep (Locale.print_locales b o Toplevel.theory_of)));
  67.746  
  67.747  val _ =
  67.748 -  Outer_Syntax.command @{command_spec "print_classes"}
  67.749 +  Outer_Syntax.command @{command_keyword print_classes}
  67.750      "print classes of this theory"
  67.751      (Scan.succeed (Toplevel.unknown_theory o
  67.752        Toplevel.keep (Class.print_classes o Toplevel.context_of)));
  67.753  
  67.754  val _ =
  67.755 -  Outer_Syntax.command @{command_spec "print_locale"}
  67.756 +  Outer_Syntax.command @{command_keyword print_locale}
  67.757      "print locale of this theory"
  67.758      (Parse.opt_bang -- Parse.position Parse.xname >> (fn (b, name) =>
  67.759        Toplevel.unknown_theory o
  67.760        Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name)));
  67.761  
  67.762  val _ =
  67.763 -  Outer_Syntax.command @{command_spec "print_interps"}
  67.764 +  Outer_Syntax.command @{command_keyword print_interps}
  67.765      "print interpretations of locale for this theory or proof context"
  67.766      (Parse.position Parse.xname >> (fn name =>
  67.767        Toplevel.unknown_context o
  67.768        Toplevel.keep (fn state => Locale.print_registrations (Toplevel.context_of state) name)));
  67.769  
  67.770  val _ =
  67.771 -  Outer_Syntax.command @{command_spec "print_dependencies"}
  67.772 +  Outer_Syntax.command @{command_keyword print_dependencies}
  67.773      "print dependencies of locale expression"
  67.774      (Parse.opt_bang -- Parse_Spec.locale_expression true >> (fn (b, expr) =>
  67.775        Toplevel.unknown_context o
  67.776        Toplevel.keep (fn state => Expression.print_dependencies (Toplevel.context_of state) b expr)));
  67.777  
  67.778  val _ =
  67.779 -  Outer_Syntax.command @{command_spec "print_attributes"}
  67.780 +  Outer_Syntax.command @{command_keyword print_attributes}
  67.781      "print attributes of this theory"
  67.782      (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
  67.783        Toplevel.keep (Attrib.print_attributes b o Toplevel.context_of)));
  67.784  
  67.785  val _ =
  67.786 -  Outer_Syntax.command @{command_spec "print_simpset"}
  67.787 +  Outer_Syntax.command @{command_keyword print_simpset}
  67.788      "print context of Simplifier"
  67.789      (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
  67.790        Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset b o Toplevel.context_of)));
  67.791  
  67.792  val _ =
  67.793 -  Outer_Syntax.command @{command_spec "print_rules"} "print intro/elim rules"
  67.794 +  Outer_Syntax.command @{command_keyword print_rules} "print intro/elim rules"
  67.795      (Scan.succeed (Toplevel.unknown_context o
  67.796        Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
  67.797  
  67.798  val _ =
  67.799 -  Outer_Syntax.command @{command_spec "print_methods"} "print methods of this theory"
  67.800 +  Outer_Syntax.command @{command_keyword print_methods} "print methods of this theory"
  67.801      (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
  67.802        Toplevel.keep (Method.print_methods b o Toplevel.context_of)));
  67.803  
  67.804  val _ =
  67.805 -  Outer_Syntax.command @{command_spec "print_antiquotations"}
  67.806 +  Outer_Syntax.command @{command_keyword print_antiquotations}
  67.807      "print document antiquotations"
  67.808      (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
  67.809        Toplevel.keep (Thy_Output.print_antiquotations b o Toplevel.context_of)));
  67.810  
  67.811  val _ =
  67.812 -  Outer_Syntax.command @{command_spec "print_ML_antiquotations"}
  67.813 +  Outer_Syntax.command @{command_keyword print_ML_antiquotations}
  67.814      "print ML antiquotations"
  67.815      (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
  67.816        Toplevel.keep (ML_Context.print_antiquotations b o Toplevel.context_of)));
  67.817  
  67.818  val _ =
  67.819 -  Outer_Syntax.command @{command_spec "thy_deps"} "visualize theory dependencies"
  67.820 +  Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies"
  67.821      (Scan.succeed Isar_Cmd.thy_deps);
  67.822  
  67.823  val _ =
  67.824 -  Outer_Syntax.command @{command_spec "locale_deps"} "visualize locale dependencies"
  67.825 +  Outer_Syntax.command @{command_keyword locale_deps} "visualize locale dependencies"
  67.826      (Scan.succeed Isar_Cmd.locale_deps);
  67.827  
  67.828  val _ =
  67.829 -  Outer_Syntax.command @{command_spec "print_term_bindings"}
  67.830 +  Outer_Syntax.command @{command_keyword print_term_bindings}
  67.831      "print term bindings of proof context"
  67.832      (Scan.succeed (Toplevel.unknown_context o
  67.833        Toplevel.keep
  67.834          (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
  67.835  
  67.836  val _ =
  67.837 -  Outer_Syntax.command @{command_spec "print_facts"} "print facts of proof context"
  67.838 +  Outer_Syntax.command @{command_keyword print_facts} "print facts of proof context"
  67.839      (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
  67.840        Toplevel.keep (Proof_Context.print_local_facts b o Toplevel.context_of)));
  67.841  
  67.842  val _ =
  67.843 -  Outer_Syntax.command @{command_spec "print_cases"} "print cases of proof context"
  67.844 +  Outer_Syntax.command @{command_keyword print_cases} "print cases of proof context"
  67.845      (Scan.succeed (Toplevel.unknown_context o
  67.846        Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of)));
  67.847  
  67.848  val _ =
  67.849 -  Outer_Syntax.command @{command_spec "print_statement"}
  67.850 +  Outer_Syntax.command @{command_keyword print_statement}
  67.851      "print theorems as long statements"
  67.852      (opt_modes -- Parse.xthms1 >> Isar_Cmd.print_stmts);
  67.853  
  67.854  val _ =
  67.855 -  Outer_Syntax.command @{command_spec "thm"} "print theorems"
  67.856 +  Outer_Syntax.command @{command_keyword thm} "print theorems"
  67.857      (opt_modes -- Parse.xthms1 >> Isar_Cmd.print_thms);
  67.858  
  67.859  val _ =
  67.860 -  Outer_Syntax.command @{command_spec "prf"} "print proof terms of theorems"
  67.861 +  Outer_Syntax.command @{command_keyword prf} "print proof terms of theorems"
  67.862      (opt_modes -- Scan.option Parse.xthms1 >> Isar_Cmd.print_prfs false);
  67.863  
  67.864  val _ =
  67.865 -  Outer_Syntax.command @{command_spec "full_prf"} "print full proof terms of theorems"
  67.866 +  Outer_Syntax.command @{command_keyword full_prf} "print full proof terms of theorems"
  67.867      (opt_modes -- Scan.option Parse.xthms1 >> Isar_Cmd.print_prfs true);
  67.868  
  67.869  val _ =
  67.870 -  Outer_Syntax.command @{command_spec "prop"} "read and print proposition"
  67.871 +  Outer_Syntax.command @{command_keyword prop} "read and print proposition"
  67.872      (opt_modes -- Parse.term >> Isar_Cmd.print_prop);
  67.873  
  67.874  val _ =
  67.875 -  Outer_Syntax.command @{command_spec "term"} "read and print term"
  67.876 +  Outer_Syntax.command @{command_keyword term} "read and print term"
  67.877      (opt_modes -- Parse.term >> Isar_Cmd.print_term);
  67.878  
  67.879  val _ =
  67.880 -  Outer_Syntax.command @{command_spec "typ"} "read and print type"
  67.881 +  Outer_Syntax.command @{command_keyword typ} "read and print type"
  67.882      (opt_modes -- (Parse.typ -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort))
  67.883        >> Isar_Cmd.print_type);
  67.884  
  67.885  val _ =
  67.886 -  Outer_Syntax.command @{command_spec "print_codesetup"} "print code generator setup"
  67.887 +  Outer_Syntax.command @{command_keyword print_codesetup} "print code generator setup"
  67.888      (Scan.succeed (Toplevel.unknown_theory o
  67.889        Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
  67.890  
  67.891  val _ =
  67.892 -  Outer_Syntax.command @{command_spec "print_state"}
  67.893 +  Outer_Syntax.command @{command_keyword print_state}
  67.894      "print current proof state (if present)"
  67.895      (opt_modes >> (fn modes => Toplevel.keep (Print_Mode.with_modes modes Toplevel.print_state)));
  67.896  
  67.897  val _ =
  67.898 -  Outer_Syntax.command @{command_spec "welcome"} "print welcome message"
  67.899 +  Outer_Syntax.command @{command_keyword welcome} "print welcome message"
  67.900      (Scan.succeed (Toplevel.imperative (writeln o Session.welcome)));
  67.901  
  67.902  val _ =
  67.903 -  Outer_Syntax.command @{command_spec "display_drafts"}
  67.904 +  Outer_Syntax.command @{command_keyword display_drafts}
  67.905      "display raw source files with symbols"
  67.906      (Scan.repeat1 Parse.path >> (fn names =>
  67.907        Toplevel.imperative (fn () => ignore (Present.display_drafts (map Path.explode names)))));
  67.908 @@ -881,24 +881,24 @@
  67.909  val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") [];
  67.910  
  67.911  val _ =
  67.912 -  Outer_Syntax.command @{command_spec "realizers"}
  67.913 +  Outer_Syntax.command @{command_keyword realizers}
  67.914      "specify realizers for primitive axioms / theorems, together with correctness proof"
  67.915      (Scan.repeat1 (Parse.xname -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
  67.916       (fn xs => Toplevel.theory (fn thy => Extraction.add_realizers
  67.917         (map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy)));
  67.918  
  67.919  val _ =
  67.920 -  Outer_Syntax.command @{command_spec "realizability"}
  67.921 +  Outer_Syntax.command @{command_keyword realizability}
  67.922      "add equations characterizing realizability"
  67.923      (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_realizes_eqns));
  67.924  
  67.925  val _ =
  67.926 -  Outer_Syntax.command @{command_spec "extract_type"}
  67.927 +  Outer_Syntax.command @{command_keyword extract_type}
  67.928      "add equations characterizing type of extracted program"
  67.929      (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_typeof_eqns));
  67.930  
  67.931  val _ =
  67.932 -  Outer_Syntax.command @{command_spec "extract"} "extract terms from proofs"
  67.933 +  Outer_Syntax.command @{command_keyword extract} "extract terms from proofs"
  67.934      (Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
  67.935        Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy)));
  67.936  
  67.937 @@ -907,7 +907,7 @@
  67.938  (** end **)
  67.939  
  67.940  val _ =
  67.941 -  Outer_Syntax.command @{command_spec "end"} "end context"
  67.942 +  Outer_Syntax.command @{command_keyword end} "end context"
  67.943      (Scan.succeed
  67.944        (Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o
  67.945          Toplevel.end_proof (K Proof.end_notepad)));
    68.1 --- a/src/Pure/ML/ml_antiquotations.ML	Mon Apr 06 16:30:44 2015 +0200
    68.2 +++ b/src/Pure/ML/ml_antiquotations.ML	Mon Apr 06 17:06:48 2015 +0200
    68.3 @@ -253,7 +253,7 @@
    68.4        if Keyword.is_keyword (Thy_Header.get_keywords thy) name then
    68.5          "Parse.$$$ " ^ ML_Syntax.print_string name
    68.6        else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #>
    68.7 -  ML_Antiquotation.value @{binding command_spec}
    68.8 +  ML_Antiquotation.value @{binding command_keyword}
    68.9      (Args.context -- Scan.lift (Parse.position Parse.name) >> (fn (ctxt, (name, pos)) =>
   68.10        (case Keyword.command_markup (Thy_Header.get_keywords' ctxt) name of
   68.11          SOME markup =>
    69.1 --- a/src/Pure/Tools/class_deps.ML	Mon Apr 06 16:30:44 2015 +0200
    69.2 +++ b/src/Pure/Tools/class_deps.ML	Mon Apr 06 17:06:48 2015 +0200
    69.3 @@ -46,7 +46,7 @@
    69.4    || (@{keyword "("} |-- Parse.enum "|" Parse.sort --| @{keyword ")"});
    69.5  
    69.6  val _ =
    69.7 -  Outer_Syntax.command @{command_spec "class_deps"} "visualize class dependencies"
    69.8 +  Outer_Syntax.command @{command_keyword class_deps} "visualize class dependencies"
    69.9      ((Scan.option parse_sort_list -- Scan.option parse_sort_list) >> (fn (super, sub) =>
   69.10        (Toplevel.unknown_theory o
   69.11         Toplevel.keep (fn st => class_deps_cmd (Toplevel.context_of st) super sub))));
    70.1 --- a/src/Pure/Tools/find_consts.ML	Mon Apr 06 16:30:44 2015 +0200
    70.2 +++ b/src/Pure/Tools/find_consts.ML	Mon Apr 06 17:06:48 2015 +0200
    70.3 @@ -151,7 +151,7 @@
    70.4    |> #1;
    70.5  
    70.6  val _ =
    70.7 -  Outer_Syntax.command @{command_spec "find_consts"}
    70.8 +  Outer_Syntax.command @{command_keyword find_consts}
    70.9      "find constants by name / type patterns"
   70.10      (query >> (fn spec =>
   70.11        Toplevel.keep (fn st =>
    71.1 --- a/src/Pure/Tools/find_theorems.ML	Mon Apr 06 16:30:44 2015 +0200
    71.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon Apr 06 17:06:48 2015 +0200
    71.3 @@ -535,7 +535,7 @@
    71.4    |> #1;
    71.5  
    71.6  val _ =
    71.7 -  Outer_Syntax.command @{command_spec "find_theorems"}
    71.8 +  Outer_Syntax.command @{command_keyword find_theorems}
    71.9      "find theorems meeting specified criteria"
   71.10      (options -- query >> (fn ((opt_lim, rem_dups), spec) =>
   71.11        Toplevel.keep (fn st =>
    72.1 --- a/src/Pure/Tools/named_theorems.ML	Mon Apr 06 16:30:44 2015 +0200
    72.2 +++ b/src/Pure/Tools/named_theorems.ML	Mon Apr 06 17:06:48 2015 +0200
    72.3 @@ -89,7 +89,7 @@
    72.4    in (name, lthy') end;
    72.5  
    72.6  val _ =
    72.7 -  Outer_Syntax.local_theory @{command_spec "named_theorems"}
    72.8 +  Outer_Syntax.local_theory @{command_keyword named_theorems}
    72.9      "declare named collection of theorems"
   72.10      (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >>
   72.11        fold (fn (b, descr) => snd o declare b descr));
    73.1 --- a/src/Pure/Tools/thm_deps.ML	Mon Apr 06 16:30:44 2015 +0200
    73.2 +++ b/src/Pure/Tools/thm_deps.ML	Mon Apr 06 17:06:48 2015 +0200
    73.3 @@ -44,7 +44,7 @@
    73.4    end;
    73.5  
    73.6  val _ =
    73.7 -  Outer_Syntax.command @{command_spec "thm_deps"} "visualize theorem dependencies"
    73.8 +  Outer_Syntax.command @{command_keyword thm_deps} "visualize theorem dependencies"
    73.9      (Parse.xthms1 >> (fn args =>
   73.10        Toplevel.unknown_theory o Toplevel.keep (fn state =>
   73.11          thm_deps (Toplevel.theory_of state) (Attrib.eval_thms (Toplevel.context_of state) args))));
   73.12 @@ -101,7 +101,7 @@
   73.13    in rev thms' end;
   73.14  
   73.15  val _ =
   73.16 -  Outer_Syntax.command @{command_spec "unused_thms"} "find unused theorems"
   73.17 +  Outer_Syntax.command @{command_keyword unused_thms} "find unused theorems"
   73.18      (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
   73.19         Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >> (fn opt_range =>
   73.20          Toplevel.keep (fn state =>
    74.1 --- a/src/Sequents/prover.ML	Mon Apr 06 16:30:44 2015 +0200
    74.2 +++ b/src/Sequents/prover.ML	Mon Apr 06 17:06:48 2015 +0200
    74.3 @@ -68,7 +68,7 @@
    74.4    end;
    74.5  
    74.6  val _ =
    74.7 -  Outer_Syntax.command @{command_spec "print_pack"} "print pack of classical rules"
    74.8 +  Outer_Syntax.command @{command_keyword print_pack} "print pack of classical rules"
    74.9      (Scan.succeed (Toplevel.keep (Pretty.writeln o pretty_pack o Toplevel.context_of)));
   74.10  
   74.11  
    75.1 --- a/src/Tools/Code/code_haskell.ML	Mon Apr 06 16:30:44 2015 +0200
    75.2 +++ b/src/Tools/Code/code_haskell.ML	Mon Apr 06 17:06:48 2015 +0200
    75.3 @@ -516,7 +516,7 @@
    75.4    #> fold (fold (Code_Target.add_reserved target) o snd) prelude_import_unqualified_constr);
    75.5  
    75.6  val _ =
    75.7 -  Outer_Syntax.command @{command_spec "code_monad"} "define code syntax for monads"
    75.8 +  Outer_Syntax.command @{command_keyword code_monad} "define code syntax for monads"
    75.9      (Parse.term -- Parse.name >> (fn (raw_bind, target) =>
   75.10        Toplevel.theory (add_monad target raw_bind)));
   75.11  
    76.1 --- a/src/Tools/Code/code_preproc.ML	Mon Apr 06 16:30:44 2015 +0200
    76.2 +++ b/src/Tools/Code/code_preproc.ML	Mon Apr 06 17:06:48 2015 +0200
    76.3 @@ -588,7 +588,7 @@
    76.4    end);
    76.5  
    76.6  val _ =
    76.7 -  Outer_Syntax.command @{command_spec "print_codeproc"} "print code preprocessor setup"
    76.8 +  Outer_Syntax.command @{command_keyword print_codeproc} "print code preprocessor setup"
    76.9      (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_codeproc o Toplevel.context_of)));
   76.10  
   76.11  end; (*struct*)
    77.1 --- a/src/Tools/Code/code_runtime.ML	Mon Apr 06 16:30:44 2015 +0200
    77.2 +++ b/src/Tools/Code/code_runtime.ML	Mon Apr 06 17:06:48 2015 +0200
    77.3 @@ -475,7 +475,7 @@
    77.4  in
    77.5  
    77.6  val _ =
    77.7 -  Outer_Syntax.command @{command_spec "code_reflect"}
    77.8 +  Outer_Syntax.command @{command_keyword code_reflect}
    77.9      "enrich runtime environment with generated code"
   77.10      (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- Parse.!!!  (parse_datatype
   77.11        ::: Scan.repeat (@{keyword "and"} |-- parse_datatype))) []
    78.1 --- a/src/Tools/Code/code_target.ML	Mon Apr 06 16:30:44 2015 +0200
    78.2 +++ b/src/Tools/Code/code_target.ML	Mon Apr 06 17:06:48 2015 +0200
    78.3 @@ -638,25 +638,25 @@
    78.4    :|-- (fn (all_public, raw_cs) => (code_expr_checkingP all_public raw_cs || code_expr_inP all_public raw_cs));
    78.5  
    78.6  val _ =
    78.7 -  Outer_Syntax.command @{command_spec "code_reserved"}
    78.8 +  Outer_Syntax.command @{command_keyword code_reserved}
    78.9      "declare words as reserved for target language"
   78.10      (Parse.name -- Scan.repeat1 Parse.name
   78.11        >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds));
   78.12  
   78.13  val _ =
   78.14 -  Outer_Syntax.command @{command_spec "code_identifier"} "declare mandatory names for code symbols"
   78.15 +  Outer_Syntax.command @{command_keyword code_identifier} "declare mandatory names for code symbols"
   78.16      (parse_symbol_pragmas Parse.name Parse.name Parse.name Parse.name Parse.name Parse.name
   78.17        >> (Toplevel.theory o fold set_identifiers_cmd));
   78.18  
   78.19  val _ =
   78.20 -  Outer_Syntax.command @{command_spec "code_printing"} "declare dedicated printing for code symbols"
   78.21 +  Outer_Syntax.command @{command_keyword code_printing} "declare dedicated printing for code symbols"
   78.22      (parse_symbol_pragmas (Code_Printer.parse_const_syntax) (Code_Printer.parse_tyco_syntax)
   78.23        Parse.string (Parse.minus >> K ()) (Parse.minus >> K ())
   78.24        (Parse.text -- Scan.optional (@{keyword "attach"} |-- Scan.repeat1 Parse.term) [])
   78.25        >> (Toplevel.theory o fold set_printings_cmd));
   78.26  
   78.27  val _ =
   78.28 -  Outer_Syntax.command @{command_spec "export_code"} "generate executable code for constants"
   78.29 +  Outer_Syntax.command @{command_keyword export_code} "generate executable code for constants"
   78.30      (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.context_of)));
   78.31  
   78.32  end; (*struct*)
    79.1 --- a/src/Tools/Code/code_thingol.ML	Mon Apr 06 16:30:44 2015 +0200
    79.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Apr 06 17:06:48 2015 +0200
    79.3 @@ -957,14 +957,14 @@
    79.4  in
    79.5  
    79.6  val _ =
    79.7 -  Outer_Syntax.command @{command_spec "code_thms"}
    79.8 +  Outer_Syntax.command @{command_keyword code_thms}
    79.9      "print system of code equations for code"
   79.10      (Scan.repeat1 Parse.term >> (fn cs =>
   79.11        Toplevel.unknown_context o
   79.12        Toplevel.keep (fn state => code_thms_cmd (Toplevel.context_of state) cs)));
   79.13  
   79.14  val _ =
   79.15 -  Outer_Syntax.command @{command_spec "code_deps"}
   79.16 +  Outer_Syntax.command @{command_keyword code_deps}
   79.17      "visualize dependencies of code equations for code"
   79.18      (Scan.repeat1 Parse.term >> (fn cs =>
   79.19        Toplevel.unknown_context o
    80.1 --- a/src/Tools/adhoc_overloading.ML	Mon Apr 06 16:30:44 2015 +0200
    80.2 +++ b/src/Tools/adhoc_overloading.ML	Mon Apr 06 17:06:48 2015 +0200
    80.3 @@ -233,12 +233,12 @@
    80.4    end;
    80.5  
    80.6  val _ =
    80.7 -  Outer_Syntax.local_theory @{command_spec "adhoc_overloading"}
    80.8 +  Outer_Syntax.local_theory @{command_keyword adhoc_overloading}
    80.9      "add adhoc overloading for constants / fixed variables"
   80.10      (Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) >> adhoc_overloading_cmd true);
   80.11  
   80.12  val _ =
   80.13 -  Outer_Syntax.local_theory @{command_spec "no_adhoc_overloading"}
   80.14 +  Outer_Syntax.local_theory @{command_keyword no_adhoc_overloading}
   80.15      "delete adhoc overloading for constants / fixed variables"
   80.16      (Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) >> adhoc_overloading_cmd false);
   80.17  
    81.1 --- a/src/Tools/induct.ML	Mon Apr 06 16:30:44 2015 +0200
    81.2 +++ b/src/Tools/induct.ML	Mon Apr 06 17:06:48 2015 +0200
    81.3 @@ -257,7 +257,7 @@
    81.4    end;
    81.5  
    81.6  val _ =
    81.7 -  Outer_Syntax.command @{command_spec "print_induct_rules"}
    81.8 +  Outer_Syntax.command @{command_keyword print_induct_rules}
    81.9      "print induction and cases rules"
   81.10      (Scan.succeed (Toplevel.unknown_context o
   81.11        Toplevel.keep (print_rules o Toplevel.context_of)));
    82.1 --- a/src/Tools/permanent_interpretation.ML	Mon Apr 06 16:30:44 2015 +0200
    82.2 +++ b/src/Tools/permanent_interpretation.ML	Mon Apr 06 17:06:48 2015 +0200
    82.3 @@ -95,7 +95,7 @@
    82.4  end;
    82.5  
    82.6  val _ =
    82.7 -  Outer_Syntax.local_theory_to_proof @{command_spec "permanent_interpretation"}
    82.8 +  Outer_Syntax.local_theory_to_proof @{command_keyword permanent_interpretation}
    82.9      "prove interpretation of locale expression into named theory"
   82.10      (Parse.!!! (Parse_Spec.locale_expression true) --
   82.11        Scan.optional (@{keyword "defining"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
    83.1 --- a/src/Tools/quickcheck.ML	Mon Apr 06 16:30:44 2015 +0200
    83.2 +++ b/src/Tools/quickcheck.ML	Mon Apr 06 17:06:48 2015 +0200
    83.3 @@ -527,11 +527,11 @@
    83.4    @{keyword "["} |-- Parse.list1 parse_arg --| @{keyword "]"} || Scan.succeed [];
    83.5  
    83.6  val _ =
    83.7 -  Outer_Syntax.command @{command_spec "quickcheck_params"} "set parameters for random testing"
    83.8 +  Outer_Syntax.command @{command_keyword quickcheck_params} "set parameters for random testing"
    83.9      (parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args)));
   83.10  
   83.11  val _ =
   83.12 -  Outer_Syntax.command @{command_spec "quickcheck"}
   83.13 +  Outer_Syntax.command @{command_keyword quickcheck}
   83.14      "try to find counterexample for subgoal"
   83.15      (parse_args -- Scan.optional Parse.nat 1 >> (fn (args, i) =>
   83.16        Toplevel.unknown_proof o Toplevel.keep (quickcheck_cmd args i)));
    84.1 --- a/src/Tools/solve_direct.ML	Mon Apr 06 16:30:44 2015 +0200
    84.2 +++ b/src/Tools/solve_direct.ML	Mon Apr 06 17:06:48 2015 +0200
    84.3 @@ -92,7 +92,7 @@
    84.4  val solve_direct = do_solve_direct Normal
    84.5  
    84.6  val _ =
    84.7 -  Outer_Syntax.command @{command_spec "solve_direct"}
    84.8 +  Outer_Syntax.command @{command_keyword solve_direct}
    84.9      "try to solve conjectures directly with existing theorems"
   84.10      (Scan.succeed (Toplevel.unknown_proof o
   84.11        Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
    85.1 --- a/src/Tools/subtyping.ML	Mon Apr 06 16:30:44 2015 +0200
    85.2 +++ b/src/Tools/subtyping.ML	Mon Apr 06 17:06:48 2015 +0200
    85.3 @@ -1115,7 +1115,7 @@
    85.4  (* outer syntax commands *)
    85.5  
    85.6  val _ =
    85.7 -  Outer_Syntax.command @{command_spec "print_coercions"}
    85.8 +  Outer_Syntax.command @{command_keyword print_coercions}
    85.9      "print information about coercions"
   85.10      (Scan.succeed (Toplevel.keep (print_coercions o Toplevel.context_of)));
   85.11  
    86.1 --- a/src/Tools/try.ML	Mon Apr 06 16:30:44 2015 +0200
    86.2 +++ b/src/Tools/try.ML	Mon Apr 06 17:06:48 2015 +0200
    86.3 @@ -75,7 +75,7 @@
    86.4      |> tap (fn NONE => writeln "Tried in vain." | _ => ())
    86.5  
    86.6  val _ =
    86.7 -  Outer_Syntax.command @{command_spec "try"}
    86.8 +  Outer_Syntax.command @{command_keyword try}
    86.9      "try a combination of automatic proving and disproving tools"
   86.10      (Scan.succeed (Toplevel.unknown_proof o Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
   86.11  
    87.1 --- a/src/ZF/Tools/datatype_package.ML	Mon Apr 06 16:30:44 2015 +0200
    87.2 +++ b/src/ZF/Tools/datatype_package.ML	Mon Apr 06 17:06:48 2015 +0200
    87.3 @@ -430,7 +430,7 @@
    87.4  
    87.5  val _ =
    87.6    Outer_Syntax.command
    87.7 -    (if coind then @{command_spec "codatatype"} else @{command_spec "datatype"})
    87.8 +    (if coind then @{command_keyword codatatype} else @{command_keyword datatype})
    87.9      ("define " ^ coind_prefix ^ "datatype")
   87.10      ((Scan.optional ((@{keyword "\<subseteq>"} || @{keyword "<="}) |-- Parse.!!! Parse.term) "") --
   87.11        Parse.and_list1 (Parse.term -- (@{keyword "="} |-- Parse.enum1 "|" con_decl)) --
    88.1 --- a/src/ZF/Tools/ind_cases.ML	Mon Apr 06 16:30:44 2015 +0200
    88.2 +++ b/src/ZF/Tools/ind_cases.ML	Mon Apr 06 17:06:48 2015 +0200
    88.3 @@ -53,7 +53,7 @@
    88.4    in thy |> Global_Theory.note_thmss "" facts |> snd end;
    88.5  
    88.6  val _ =
    88.7 -  Outer_Syntax.command @{command_spec "inductive_cases"}
    88.8 +  Outer_Syntax.command @{command_keyword inductive_cases}
    88.9      "create simplified instances of elimination rules (improper)"
   88.10      (Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Scan.repeat1 Parse.prop)
   88.11        >> (Toplevel.theory o inductive_cases));
    89.1 --- a/src/ZF/Tools/induct_tacs.ML	Mon Apr 06 16:30:44 2015 +0200
    89.2 +++ b/src/ZF/Tools/induct_tacs.ML	Mon Apr 06 17:06:48 2015 +0200
    89.3 @@ -191,7 +191,7 @@
    89.4  (* outer syntax *)
    89.5  
    89.6  val _ =
    89.7 -  Outer_Syntax.command @{command_spec "rep_datatype"} "represent existing set inductively"
    89.8 +  Outer_Syntax.command @{command_keyword rep_datatype} "represent existing set inductively"
    89.9      ((@{keyword "elimination"} |-- Parse.!!! Parse.xthm) --
   89.10       (@{keyword "induction"} |-- Parse.!!! Parse.xthm) --
   89.11       (@{keyword "case_eqns"} |-- Parse.!!! Parse.xthms1) --
    90.1 --- a/src/ZF/Tools/inductive_package.ML	Mon Apr 06 16:30:44 2015 +0200
    90.2 +++ b/src/ZF/Tools/inductive_package.ML	Mon Apr 06 17:06:48 2015 +0200
    90.3 @@ -595,7 +595,7 @@
    90.4  
    90.5  val _ =
    90.6    Outer_Syntax.command
    90.7 -    (if coind then @{command_spec "coinductive"} else @{command_spec "inductive"})
    90.8 +    (if coind then @{command_keyword coinductive} else @{command_keyword inductive})
    90.9      ("define " ^ co_prefix ^ "inductive sets") ind_decl;
   90.10  
   90.11  end;
    91.1 --- a/src/ZF/Tools/primrec_package.ML	Mon Apr 06 16:30:44 2015 +0200
    91.2 +++ b/src/ZF/Tools/primrec_package.ML	Mon Apr 06 17:06:48 2015 +0200
    91.3 @@ -197,7 +197,7 @@
    91.4  (* outer syntax *)
    91.5  
    91.6  val _ =
    91.7 -  Outer_Syntax.command @{command_spec "primrec"} "define primitive recursive functions on datatypes"
    91.8 +  Outer_Syntax.command @{command_keyword primrec} "define primitive recursive functions on datatypes"
    91.9      (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)
   91.10        >> (Toplevel.theory o (#1 oo (add_primrec o map Parse.triple_swap))));
   91.11  
    92.1 --- a/src/ZF/Tools/typechk.ML	Mon Apr 06 16:30:44 2015 +0200
    92.2 +++ b/src/ZF/Tools/typechk.ML	Mon Apr 06 17:06:48 2015 +0200
    92.3 @@ -126,7 +126,7 @@
    92.4        "ZF type-checking");
    92.5  
    92.6  val _ =
    92.7 -  Outer_Syntax.command @{command_spec "print_tcset"} "print context of ZF typecheck"
    92.8 +  Outer_Syntax.command @{command_keyword print_tcset} "print context of ZF typecheck"
    92.9      (Scan.succeed (Toplevel.unknown_context o
   92.10        Toplevel.keep (print_tcset o Toplevel.context_of)));
   92.11