eliminated unused int_only flag (see also c12484a27367);
authorwenzelm
Mon Nov 03 14:50:27 2014 +0100 (2014-11-03)
changeset 588939e0ecb66d6a7
parent 58892 20aa19ecf2cc
child 58894 447972249785
eliminated unused int_only flag (see also c12484a27367);
just proper commands;
src/HOL/Decision_Procs/approximation.ML
src/HOL/Library/Old_SMT/old_smt_config.ML
src/HOL/Library/refute.ML
src/HOL/Orderings.thy
src/HOL/SPARK/Tools/spark_commands.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/Ctr_Sugar/case_translation.ML
src/HOL/Tools/Lifting/lifting_info.ML
src/HOL/Tools/Nitpick/nitpick_commands.ML
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Predicate_Compile/predicate_compile.ML
src/HOL/Tools/Quickcheck/find_unused_assms.ML
src/HOL/Tools/Quotient/quotient_info.ML
src/HOL/Tools/SMT/smt_config.ML
src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/try0.ML
src/HOL/Tools/value.ML
src/HOL/ex/Cartouche_Examples.thy
src/Provers/classical.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/toplevel.ML
src/Pure/Tools/class_deps.ML
src/Pure/Tools/find_consts.ML
src/Pure/Tools/find_theorems.ML
src/Pure/Tools/thm_deps.ML
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_thingol.ML
src/Tools/induct.ML
src/Tools/quickcheck.ML
src/Tools/solve_direct.ML
src/Tools/subtyping.ML
src/Tools/try.ML
src/ZF/Tools/typechk.ML
     1.1 --- a/src/HOL/Decision_Procs/approximation.ML	Mon Nov 03 14:31:15 2014 +0100
     1.2 +++ b/src/HOL/Decision_Procs/approximation.ML	Mon Nov 03 14:50:27 2014 +0100
     1.3 @@ -151,7 +151,7 @@
     1.4    Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
     1.5  
     1.6  val _ =
     1.7 -  Outer_Syntax.improper_command @{command_spec "approximate"} "print approximation of term"
     1.8 +  Outer_Syntax.command @{command_spec "approximate"} "print approximation of term"
     1.9      (opt_modes -- Parse.term
    1.10        >> (fn (modes, t) => Toplevel.keep (approximate_cmd modes t)));
    1.11  
     2.1 --- a/src/HOL/Library/Old_SMT/old_smt_config.ML	Mon Nov 03 14:31:15 2014 +0100
     2.2 +++ b/src/HOL/Library/Old_SMT/old_smt_config.ML	Mon Nov 03 14:50:27 2014 +0100
     2.3 @@ -246,7 +246,7 @@
     2.4    end
     2.5  
     2.6  val _ =
     2.7 -  Outer_Syntax.improper_command @{command_spec "old_smt_status"}
     2.8 +  Outer_Syntax.command @{command_spec "old_smt_status"}
     2.9      "show the available SMT solvers, the currently selected SMT solver, \
    2.10      \and the values of SMT configuration options"
    2.11      (Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of)))
     3.1 --- a/src/HOL/Library/refute.ML	Mon Nov 03 14:31:15 2014 +0100
     3.2 +++ b/src/HOL/Library/refute.ML	Mon Nov 03 14:50:27 2014 +0100
     3.3 @@ -2967,7 +2967,7 @@
     3.4  (* 'refute' command *)
     3.5  
     3.6  val _ =
     3.7 -  Outer_Syntax.improper_command @{command_spec "refute"}
     3.8 +  Outer_Syntax.command @{command_spec "refute"}
     3.9      "try to find a model that refutes a given subgoal"
    3.10      (scan_parms -- Scan.optional Parse.nat 1 >>
    3.11        (fn (parms, i) =>
     4.1 --- a/src/HOL/Orderings.thy	Mon Nov 03 14:31:15 2014 +0100
     4.2 +++ b/src/HOL/Orderings.thy	Mon Nov 03 14:50:27 2014 +0100
     4.3 @@ -439,7 +439,7 @@
     4.4    end;
     4.5  
     4.6  val _ =
     4.7 -  Outer_Syntax.improper_command @{command_spec "print_orders"}
     4.8 +  Outer_Syntax.command @{command_spec "print_orders"}
     4.9      "print order structures available to transitivity reasoner"
    4.10      (Scan.succeed (Toplevel.unknown_context o
    4.11        Toplevel.keep (print_structures o Toplevel.context_of)));
     5.1 --- a/src/HOL/SPARK/Tools/spark_commands.ML	Mon Nov 03 14:31:15 2014 +0100
     5.2 +++ b/src/HOL/SPARK/Tools/spark_commands.ML	Mon Nov 03 14:50:27 2014 +0100
     5.3 @@ -126,7 +126,7 @@
     5.4      (Parse.name >> (fn name => Toplevel.local_theory_to_proof NONE (prove_vc name)));
     5.5  
     5.6  val _ =
     5.7 -  Outer_Syntax.improper_command @{command_spec "spark_status"}
     5.8 +  Outer_Syntax.command @{command_spec "spark_status"}
     5.9      "show the name and state of all loaded verification conditions"
    5.10      (Scan.optional
    5.11         (Args.parens
     6.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Mon Nov 03 14:31:15 2014 +0100
     6.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Mon Nov 03 14:50:27 2014 +0100
     6.3 @@ -912,7 +912,7 @@
     6.4    in TPTP_Data.map (cons ((prob_name, result))) thy' end
     6.5  
     6.6  val _ =
     6.7 -  Outer_Syntax.improper_command @{command_spec "import_tptp"} "import TPTP problem"
     6.8 +  Outer_Syntax.command @{command_spec "import_tptp"} "import TPTP problem"
     6.9      (Parse.path >> (fn name =>
    6.10        Toplevel.theory (fn thy =>
    6.11          let val path = Path.explode name
     7.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Mon Nov 03 14:31:15 2014 +0100
     7.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Mon Nov 03 14:50:27 2014 +0100
     7.3 @@ -1866,7 +1866,7 @@
     7.4  
     7.5  (*This has been disabled since it requires a hook to be specified to use "import_thm"
     7.6  val _ =
     7.7 -  Outer_Syntax.improper_command @{command_spec "import_leo2_proof"} "import TPTP proof"
     7.8 +  Outer_Syntax.command @{command_spec "import_leo2_proof"} "import TPTP proof"
     7.9      (Parse.path >> (fn name =>
    7.10        Toplevel.theory (fn thy =>
    7.11         let val path = Path.explode name
     8.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Mon Nov 03 14:31:15 2014 +0100
     8.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Nov 03 14:50:27 2014 +0100
     8.3 @@ -1598,7 +1598,7 @@
     8.4    end;
     8.5  
     8.6  val _ =
     8.7 -  Outer_Syntax.improper_command @{command_spec "print_bnfs"}
     8.8 +  Outer_Syntax.command @{command_spec "print_bnfs"}
     8.9      "print all bounded natural functors"
    8.10      (Scan.succeed (Toplevel.keep (print_bnfs o Toplevel.context_of)));
    8.11  
     9.1 --- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Mon Nov 03 14:31:15 2014 +0100
     9.2 +++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Mon Nov 03 14:50:27 2014 +0100
     9.3 @@ -630,7 +630,7 @@
     9.4    end;
     9.5  
     9.6  val _ =
     9.7 -  Outer_Syntax.improper_command @{command_spec "print_case_translations"}
     9.8 +  Outer_Syntax.command @{command_spec "print_case_translations"}
     9.9      "print registered case combinators and constructors"
    9.10      (Scan.succeed (Toplevel.keep (print_case_translations o Toplevel.context_of)))
    9.11  
    10.1 --- a/src/HOL/Tools/Lifting/lifting_info.ML	Mon Nov 03 14:31:15 2014 +0100
    10.2 +++ b/src/HOL/Tools/Lifting/lifting_info.ML	Mon Nov 03 14:50:27 2014 +0100
    10.3 @@ -532,11 +532,11 @@
    10.4  (* outer syntax commands *)
    10.5  
    10.6  val _ =
    10.7 -  Outer_Syntax.improper_command @{command_spec "print_quot_maps"} "print quotient map functions"
    10.8 +  Outer_Syntax.command @{command_spec "print_quot_maps"} "print quotient map functions"
    10.9      (Scan.succeed (Toplevel.keep (print_quot_maps o Toplevel.context_of)))
   10.10  
   10.11  val _ =
   10.12 -  Outer_Syntax.improper_command @{command_spec "print_quotients"} "print quotients"
   10.13 +  Outer_Syntax.command @{command_spec "print_quotients"} "print quotients"
   10.14      (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
   10.15  
   10.16  end
    11.1 --- a/src/HOL/Tools/Nitpick/nitpick_commands.ML	Mon Nov 03 14:31:15 2014 +0100
    11.2 +++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML	Mon Nov 03 14:50:27 2014 +0100
    11.3 @@ -374,7 +374,7 @@
    11.4                                        |> sort_strings |> cat_lines)))))
    11.5  
    11.6  val _ =
    11.7 -  Outer_Syntax.improper_command @{command_spec "nitpick"}
    11.8 +  Outer_Syntax.command @{command_spec "nitpick"}
    11.9      "try to find a counterexample for a given subgoal using Nitpick"
   11.10      (parse_params -- Scan.optional Parse.nat 1 >> (fn (params, i) =>
   11.11        Toplevel.unknown_proof o
    12.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Nov 03 14:31:15 2014 +0100
    12.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Nov 03 14:50:27 2014 +0100
    12.3 @@ -1028,7 +1028,7 @@
    12.4    Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []
    12.5  
    12.6  val _ =
    12.7 -  Outer_Syntax.improper_command @{command_spec "values_prolog"}
    12.8 +  Outer_Syntax.command @{command_spec "values_prolog"}
    12.9      "enumerate and print comprehensions"
   12.10      (opt_print_modes -- Scan.optional (Parse.nat >> SOME) NONE -- Parse.term
   12.11       >> (fn ((print_modes, soln), t) => Toplevel.keep (values_cmd print_modes soln t)))
    13.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon Nov 03 14:31:15 2014 +0100
    13.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon Nov 03 14:50:27 2014 +0100
    13.3 @@ -287,7 +287,7 @@
    13.4      (opt_expected_modes -- opt_modes -- scan_options -- Parse.term >> code_pred_cmd)
    13.5  
    13.6  val _ =
    13.7 -  Outer_Syntax.improper_command @{command_spec "values"}
    13.8 +  Outer_Syntax.command @{command_spec "values"}
    13.9      "enumerate and print comprehensions"
   13.10      (opt_print_modes -- opt_param_modes -- value_options -- Scan.optional Parse.nat ~1 -- Parse.term
   13.11        >> (fn ((((print_modes, param_modes), options), k), t) => Toplevel.keep
    14.1 --- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Mon Nov 03 14:31:15 2014 +0100
    14.2 +++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Mon Nov 03 14:50:27 2014 +0100
    14.3 @@ -111,7 +111,7 @@
    14.4  end
    14.5  
    14.6  val _ =
    14.7 -  Outer_Syntax.improper_command @{command_spec "find_unused_assms"}
    14.8 +  Outer_Syntax.command @{command_spec "find_unused_assms"}
    14.9      "find theorems with (potentially) superfluous assumptions"
   14.10      (Scan.option Parse.name >> (fn name =>
   14.11        Toplevel.keep (fn state => print_unused_assms (Toplevel.context_of state) name)))
    15.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Mon Nov 03 14:31:15 2014 +0100
    15.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Mon Nov 03 14:50:27 2014 +0100
    15.3 @@ -229,15 +229,15 @@
    15.4  (* outer syntax commands *)
    15.5  
    15.6  val _ =
    15.7 -  Outer_Syntax.improper_command @{command_spec "print_quotmapsQ3"} "print quotient map functions"
    15.8 +  Outer_Syntax.command @{command_spec "print_quotmapsQ3"} "print quotient map functions"
    15.9      (Scan.succeed (Toplevel.keep (print_quotmaps o Toplevel.context_of)))
   15.10  
   15.11  val _ =
   15.12 -  Outer_Syntax.improper_command @{command_spec "print_quotientsQ3"} "print quotients"
   15.13 +  Outer_Syntax.command @{command_spec "print_quotientsQ3"} "print quotients"
   15.14      (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
   15.15  
   15.16  val _ =
   15.17 -  Outer_Syntax.improper_command @{command_spec "print_quotconsts"} "print quotient constants"
   15.18 +  Outer_Syntax.command @{command_spec "print_quotconsts"} "print quotient constants"
   15.19      (Scan.succeed (Toplevel.keep (print_quotconsts o Toplevel.context_of)))
   15.20  
   15.21  end;
    16.1 --- a/src/HOL/Tools/SMT/smt_config.ML	Mon Nov 03 14:31:15 2014 +0100
    16.2 +++ b/src/HOL/Tools/SMT/smt_config.ML	Mon Nov 03 14:50:27 2014 +0100
    16.3 @@ -241,7 +241,7 @@
    16.4    end
    16.5  
    16.6  val _ =
    16.7 -  Outer_Syntax.improper_command @{command_spec "smt_status"}
    16.8 +  Outer_Syntax.command @{command_spec "smt_status"}
    16.9      "show the available SMT solvers, the currently selected SMT solver, \
   16.10      \and the values of SMT configuration options"
   16.11      (Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of)))
    17.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Nov 03 14:31:15 2014 +0100
    17.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Nov 03 14:50:27 2014 +0100
    17.3 @@ -386,7 +386,7 @@
    17.4      no_fact_override
    17.5  
    17.6  val _ =
    17.7 -  Outer_Syntax.improper_command @{command_spec "sledgehammer"}
    17.8 +  Outer_Syntax.command @{command_spec "sledgehammer"}
    17.9      "search for first-order proof using automatic theorem provers"
   17.10      ((Scan.optional Parse.name runN -- parse_params
   17.11        -- parse_fact_override -- Scan.option Parse.nat) #>> sledgehammer_trans)
    18.1 --- a/src/HOL/Tools/inductive.ML	Mon Nov 03 14:31:15 2014 +0100
    18.2 +++ b/src/HOL/Tools/inductive.ML	Mon Nov 03 14:50:27 2014 +0100
    18.3 @@ -1179,7 +1179,7 @@
    18.4      (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_simps));
    18.5  
    18.6  val _ =
    18.7 -  Outer_Syntax.improper_command @{command_spec "print_inductives"}
    18.8 +  Outer_Syntax.command @{command_spec "print_inductives"}
    18.9      "print (co)inductive definitions and monotonicity rules"
   18.10      (Scan.succeed (Toplevel.unknown_context o
   18.11        Toplevel.keep (print_inductives o Toplevel.context_of)));
    19.1 --- a/src/HOL/Tools/try0.ML	Mon Nov 03 14:31:15 2014 +0100
    19.2 +++ b/src/HOL/Tools/try0.ML	Mon Nov 03 14:50:27 2014 +0100
    19.3 @@ -180,7 +180,7 @@
    19.4     || Scan.repeat parse_attr >> (fn quad => fold merge_attrs quad ([], [], [], []))) x;
    19.5  
    19.6  val _ =
    19.7 -  Outer_Syntax.improper_command @{command_spec "try0"} "try a combination of proof methods"
    19.8 +  Outer_Syntax.command @{command_spec "try0"} "try a combination of proof methods"
    19.9      (Scan.optional parse_attrs ([], [], [], []) #>> try0_trans);
   19.10  
   19.11  fun try_try0 auto = generic_try0 (if auto then Auto_Try else Try) NONE ([], [], [], []);
    20.1 --- a/src/HOL/Tools/value.ML	Mon Nov 03 14:31:15 2014 +0100
    20.2 +++ b/src/HOL/Tools/value.ML	Mon Nov 03 14:50:27 2014 +0100
    20.3 @@ -70,7 +70,7 @@
    20.4    Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"})
    20.5    
    20.6  val _ =
    20.7 -  Outer_Syntax.improper_command @{command_spec "value"} "evaluate and print term"
    20.8 +  Outer_Syntax.command @{command_spec "value"} "evaluate and print term"
    20.9      (opt_evaluator -- opt_modes -- Parse.term
   20.10        >> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t)));
   20.11  
    21.1 --- a/src/HOL/ex/Cartouche_Examples.thy	Mon Nov 03 14:31:15 2014 +0100
    21.2 +++ b/src/HOL/ex/Cartouche_Examples.thy	Mon Nov 03 14:50:27 2014 +0100
    21.3 @@ -36,7 +36,7 @@
    21.4  subsection {* Outer syntax: cartouche within command syntax *}
    21.5  
    21.6  ML {*
    21.7 -  Outer_Syntax.improper_command @{command_spec "cartouche"} ""
    21.8 +  Outer_Syntax.command @{command_spec "cartouche"} ""
    21.9      (Parse.cartouche >> (fn s =>
   21.10        Toplevel.imperative (fn () => writeln s)))
   21.11  *}
   21.12 @@ -112,7 +112,7 @@
   21.13  subsubsection {* Term cartouche and regular quotes *}
   21.14  
   21.15  ML {*
   21.16 -  Outer_Syntax.improper_command @{command_spec "term_cartouche"} ""
   21.17 +  Outer_Syntax.command @{command_spec "term_cartouche"} ""
   21.18      (Parse.inner_syntax Parse.cartouche >> (fn s =>
   21.19        Toplevel.keep (fn state =>
   21.20          let
    22.1 --- a/src/Provers/classical.ML	Mon Nov 03 14:31:15 2014 +0100
    22.2 +++ b/src/Provers/classical.ML	Mon Nov 03 14:50:27 2014 +0100
    22.3 @@ -980,7 +980,7 @@
    22.4  (** outer syntax **)
    22.5  
    22.6  val _ =
    22.7 -  Outer_Syntax.improper_command @{command_spec "print_claset"} "print context of Classical Reasoner"
    22.8 +  Outer_Syntax.command @{command_spec "print_claset"} "print context of Classical Reasoner"
    22.9      (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_claset o Toplevel.context_of)));
   22.10  
   22.11  end;
    23.1 --- a/src/Pure/Isar/calculation.ML	Mon Nov 03 14:31:15 2014 +0100
    23.2 +++ b/src/Pure/Isar/calculation.ML	Mon Nov 03 14:50:27 2014 +0100
    23.3 @@ -222,7 +222,7 @@
    23.4      (Scan.succeed (Toplevel.proof' ultimately));
    23.5  
    23.6  val _ =
    23.7 -  Outer_Syntax.improper_command @{command_spec "print_trans_rules"} "print transitivity rules"
    23.8 +  Outer_Syntax.command @{command_spec "print_trans_rules"} "print transitivity rules"
    23.9      (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_rules o Toplevel.context_of)));
   23.10  
   23.11  end;
    24.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Nov 03 14:31:15 2014 +0100
    24.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Nov 03 14:50:27 2014 +0100
    24.3 @@ -397,7 +397,7 @@
    24.4      (Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.including_cmd));
    24.5  
    24.6  val _ =
    24.7 -  Outer_Syntax.improper_command @{command_spec "print_bundles"}
    24.8 +  Outer_Syntax.command @{command_spec "print_bundles"}
    24.9      "print bundles of declarations"
   24.10      (Scan.succeed (Toplevel.unknown_context o
   24.11        Toplevel.keep (Bundle.print_bundles o Toplevel.context_of)));
   24.12 @@ -727,194 +727,194 @@
   24.13  val opt_bang = Scan.optional (@{keyword "!"} >> K true) false;
   24.14  
   24.15  val _ =
   24.16 -  Outer_Syntax.improper_command @{command_spec "help"}
   24.17 +  Outer_Syntax.command @{command_spec "help"}
   24.18      "retrieve outer syntax commands according to name patterns"
   24.19      (Scan.repeat Parse.name >>
   24.20        (fn pats => Toplevel.imperative (fn () => Outer_Syntax.help_syntax pats)));
   24.21  
   24.22  val _ =
   24.23 -  Outer_Syntax.improper_command @{command_spec "print_commands"} "print outer syntax commands"
   24.24 +  Outer_Syntax.command @{command_spec "print_commands"} "print outer syntax commands"
   24.25      (Scan.succeed (Toplevel.imperative Outer_Syntax.print_syntax));
   24.26  
   24.27  val _ =
   24.28 -  Outer_Syntax.improper_command @{command_spec "print_options"} "print configuration options"
   24.29 +  Outer_Syntax.command @{command_spec "print_options"} "print configuration options"
   24.30      (Scan.succeed (Toplevel.unknown_context o
   24.31        Toplevel.keep (Attrib.print_options o Toplevel.context_of)));
   24.32  
   24.33  val _ =
   24.34 -  Outer_Syntax.improper_command @{command_spec "print_context"}
   24.35 +  Outer_Syntax.command @{command_spec "print_context"}
   24.36      "print context of local theory target"
   24.37      (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_context)));
   24.38  
   24.39  val _ =
   24.40 -  Outer_Syntax.improper_command @{command_spec "print_theory"}
   24.41 +  Outer_Syntax.command @{command_spec "print_theory"}
   24.42      "print logical theory contents (verbose!)"
   24.43      (opt_bang >> (fn b => Toplevel.unknown_theory o
   24.44        Toplevel.keep (Pretty.writeln o Proof_Display.pretty_full_theory b o Toplevel.theory_of)));
   24.45  
   24.46  val _ =
   24.47 -  Outer_Syntax.improper_command @{command_spec "print_syntax"}
   24.48 +  Outer_Syntax.command @{command_spec "print_syntax"}
   24.49      "print inner syntax of context (verbose!)"
   24.50      (Scan.succeed (Toplevel.unknown_context o
   24.51        Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
   24.52  
   24.53  val _ =
   24.54 -  Outer_Syntax.improper_command @{command_spec "print_defn_rules"}
   24.55 +  Outer_Syntax.command @{command_spec "print_defn_rules"}
   24.56      "print definitional rewrite rules of context"
   24.57      (Scan.succeed (Toplevel.unknown_context o
   24.58        Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of)));
   24.59  
   24.60  val _ =
   24.61 -  Outer_Syntax.improper_command @{command_spec "print_abbrevs"}
   24.62 +  Outer_Syntax.command @{command_spec "print_abbrevs"}
   24.63      "print constant abbreviations of context"
   24.64      (Scan.succeed (Toplevel.unknown_context o
   24.65        Toplevel.keep (Proof_Context.print_abbrevs o Toplevel.context_of)));
   24.66  
   24.67  val _ =
   24.68 -  Outer_Syntax.improper_command @{command_spec "print_theorems"}
   24.69 +  Outer_Syntax.command @{command_spec "print_theorems"}
   24.70      "print theorems of local theory or proof context"
   24.71      (opt_bang >> (fn b =>
   24.72        Toplevel.unknown_context o
   24.73        Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b)));
   24.74  
   24.75  val _ =
   24.76 -  Outer_Syntax.improper_command @{command_spec "print_locales"}
   24.77 +  Outer_Syntax.command @{command_spec "print_locales"}
   24.78      "print locales of this theory"
   24.79      (Scan.succeed (Toplevel.unknown_theory o
   24.80        Toplevel.keep (Locale.print_locales o Toplevel.theory_of)));
   24.81  
   24.82  val _ =
   24.83 -  Outer_Syntax.improper_command @{command_spec "print_classes"}
   24.84 +  Outer_Syntax.command @{command_spec "print_classes"}
   24.85      "print classes of this theory"
   24.86      (Scan.succeed (Toplevel.unknown_theory o
   24.87        Toplevel.keep (Class.print_classes o Toplevel.context_of)));
   24.88  
   24.89  val _ =
   24.90 -  Outer_Syntax.improper_command @{command_spec "print_locale"}
   24.91 +  Outer_Syntax.command @{command_spec "print_locale"}
   24.92      "print locale of this theory"
   24.93      (opt_bang -- Parse.position Parse.xname >> (fn (b, name) =>
   24.94        Toplevel.unknown_theory o
   24.95        Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name)));
   24.96  
   24.97  val _ =
   24.98 -  Outer_Syntax.improper_command @{command_spec "print_interps"}
   24.99 +  Outer_Syntax.command @{command_spec "print_interps"}
  24.100      "print interpretations of locale for this theory or proof context"
  24.101      (Parse.position Parse.xname >> (fn name =>
  24.102        Toplevel.unknown_context o
  24.103        Toplevel.keep (fn state => Locale.print_registrations (Toplevel.context_of state) name)));
  24.104  
  24.105  val _ =
  24.106 -  Outer_Syntax.improper_command @{command_spec "print_dependencies"}
  24.107 +  Outer_Syntax.command @{command_spec "print_dependencies"}
  24.108      "print dependencies of locale expression"
  24.109      (opt_bang -- Parse_Spec.locale_expression true >> (fn (b, expr) =>
  24.110        Toplevel.unknown_context o
  24.111        Toplevel.keep (fn state => Expression.print_dependencies (Toplevel.context_of state) b expr)));
  24.112  
  24.113  val _ =
  24.114 -  Outer_Syntax.improper_command @{command_spec "print_attributes"}
  24.115 +  Outer_Syntax.command @{command_spec "print_attributes"}
  24.116      "print attributes of this theory"
  24.117      (Scan.succeed (Toplevel.unknown_theory o
  24.118        Toplevel.keep (Attrib.print_attributes o Toplevel.context_of)));
  24.119  
  24.120  val _ =
  24.121 -  Outer_Syntax.improper_command @{command_spec "print_simpset"}
  24.122 +  Outer_Syntax.command @{command_spec "print_simpset"}
  24.123      "print context of Simplifier"
  24.124      (Scan.succeed (Toplevel.unknown_context o
  24.125        Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset o Toplevel.context_of)));
  24.126  
  24.127  val _ =
  24.128 -  Outer_Syntax.improper_command @{command_spec "print_rules"} "print intro/elim rules"
  24.129 +  Outer_Syntax.command @{command_spec "print_rules"} "print intro/elim rules"
  24.130      (Scan.succeed (Toplevel.unknown_context o
  24.131        Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
  24.132  
  24.133  val _ =
  24.134 -  Outer_Syntax.improper_command @{command_spec "print_methods"} "print methods of this theory"
  24.135 +  Outer_Syntax.command @{command_spec "print_methods"} "print methods of this theory"
  24.136      (Scan.succeed (Toplevel.unknown_theory o
  24.137        Toplevel.keep (Method.print_methods o Toplevel.context_of)));
  24.138  
  24.139  val _ =
  24.140 -  Outer_Syntax.improper_command @{command_spec "print_antiquotations"}
  24.141 +  Outer_Syntax.command @{command_spec "print_antiquotations"}
  24.142      "print document antiquotations"
  24.143      (Scan.succeed (Toplevel.unknown_context o
  24.144        Toplevel.keep (Thy_Output.print_antiquotations o Toplevel.context_of)));
  24.145  
  24.146  val _ =
  24.147 -  Outer_Syntax.improper_command @{command_spec "print_ML_antiquotations"}
  24.148 +  Outer_Syntax.command @{command_spec "print_ML_antiquotations"}
  24.149      "print ML antiquotations"
  24.150      (Scan.succeed (Toplevel.unknown_context o
  24.151        Toplevel.keep (ML_Context.print_antiquotations o Toplevel.context_of)));
  24.152  
  24.153  val _ =
  24.154 -  Outer_Syntax.improper_command @{command_spec "thy_deps"} "visualize theory dependencies"
  24.155 +  Outer_Syntax.command @{command_spec "thy_deps"} "visualize theory dependencies"
  24.156      (Scan.succeed Isar_Cmd.thy_deps);
  24.157  
  24.158  val _ =
  24.159 -  Outer_Syntax.improper_command @{command_spec "locale_deps"} "visualize locale dependencies"
  24.160 +  Outer_Syntax.command @{command_spec "locale_deps"} "visualize locale dependencies"
  24.161      (Scan.succeed Isar_Cmd.locale_deps);
  24.162  
  24.163  val _ =
  24.164 -  Outer_Syntax.improper_command @{command_spec "print_term_bindings"}
  24.165 +  Outer_Syntax.command @{command_spec "print_term_bindings"}
  24.166      "print term bindings of proof context"
  24.167      (Scan.succeed (Toplevel.unknown_context o
  24.168        Toplevel.keep
  24.169          (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
  24.170  
  24.171  val _ =
  24.172 -  Outer_Syntax.improper_command @{command_spec "print_facts"} "print facts of proof context"
  24.173 +  Outer_Syntax.command @{command_spec "print_facts"} "print facts of proof context"
  24.174      (opt_bang >> (fn verbose => Toplevel.unknown_context o
  24.175        Toplevel.keep (fn st => Proof_Context.print_local_facts (Toplevel.context_of st) verbose)));
  24.176  
  24.177  val _ =
  24.178 -  Outer_Syntax.improper_command @{command_spec "print_cases"} "print cases of proof context"
  24.179 +  Outer_Syntax.command @{command_spec "print_cases"} "print cases of proof context"
  24.180      (Scan.succeed (Toplevel.unknown_context o
  24.181        Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of)));
  24.182  
  24.183  val _ =
  24.184 -  Outer_Syntax.improper_command @{command_spec "print_statement"}
  24.185 +  Outer_Syntax.command @{command_spec "print_statement"}
  24.186      "print theorems as long statements"
  24.187      (opt_modes -- Parse.xthms1 >> Isar_Cmd.print_stmts);
  24.188  
  24.189  val _ =
  24.190 -  Outer_Syntax.improper_command @{command_spec "thm"} "print theorems"
  24.191 +  Outer_Syntax.command @{command_spec "thm"} "print theorems"
  24.192      (opt_modes -- Parse.xthms1 >> Isar_Cmd.print_thms);
  24.193  
  24.194  val _ =
  24.195 -  Outer_Syntax.improper_command @{command_spec "prf"} "print proof terms of theorems"
  24.196 +  Outer_Syntax.command @{command_spec "prf"} "print proof terms of theorems"
  24.197      (opt_modes -- Scan.option Parse.xthms1 >> Isar_Cmd.print_prfs false);
  24.198  
  24.199  val _ =
  24.200 -  Outer_Syntax.improper_command @{command_spec "full_prf"} "print full proof terms of theorems"
  24.201 +  Outer_Syntax.command @{command_spec "full_prf"} "print full proof terms of theorems"
  24.202      (opt_modes -- Scan.option Parse.xthms1 >> Isar_Cmd.print_prfs true);
  24.203  
  24.204  val _ =
  24.205 -  Outer_Syntax.improper_command @{command_spec "prop"} "read and print proposition"
  24.206 +  Outer_Syntax.command @{command_spec "prop"} "read and print proposition"
  24.207      (opt_modes -- Parse.term >> Isar_Cmd.print_prop);
  24.208  
  24.209  val _ =
  24.210 -  Outer_Syntax.improper_command @{command_spec "term"} "read and print term"
  24.211 +  Outer_Syntax.command @{command_spec "term"} "read and print term"
  24.212      (opt_modes -- Parse.term >> Isar_Cmd.print_term);
  24.213  
  24.214  val _ =
  24.215 -  Outer_Syntax.improper_command @{command_spec "typ"} "read and print type"
  24.216 +  Outer_Syntax.command @{command_spec "typ"} "read and print type"
  24.217      (opt_modes -- (Parse.typ -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort))
  24.218        >> Isar_Cmd.print_type);
  24.219  
  24.220  val _ =
  24.221 -  Outer_Syntax.improper_command @{command_spec "print_codesetup"} "print code generator setup"
  24.222 +  Outer_Syntax.command @{command_spec "print_codesetup"} "print code generator setup"
  24.223      (Scan.succeed (Toplevel.unknown_theory o
  24.224        Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
  24.225  
  24.226  val _ =
  24.227 -  Outer_Syntax.improper_command @{command_spec "print_state"}
  24.228 +  Outer_Syntax.command @{command_spec "print_state"}
  24.229      "print current proof state (if present)"
  24.230      (opt_modes >> (fn modes => Toplevel.keep (Print_Mode.with_modes modes Toplevel.print_state)));
  24.231  
  24.232  val _ =
  24.233 -  Outer_Syntax.improper_command @{command_spec "welcome"} "print welcome message"
  24.234 +  Outer_Syntax.command @{command_spec "welcome"} "print welcome message"
  24.235      (Scan.succeed (Toplevel.imperative (writeln o Session.welcome)));
  24.236  
  24.237  val _ =
  24.238 -  Outer_Syntax.improper_command @{command_spec "display_drafts"}
  24.239 +  Outer_Syntax.command @{command_spec "display_drafts"}
  24.240      "display raw source files with symbols"
  24.241      (Scan.repeat1 Parse.path >> (fn names =>
  24.242        Toplevel.imperative (fn () => ignore (Present.display_drafts (map Path.explode names)))));
    25.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon Nov 03 14:31:15 2014 +0100
    25.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon Nov 03 14:50:27 2014 +0100
    25.3 @@ -19,8 +19,6 @@
    25.4      (Toplevel.transition -> Toplevel.transition) parser -> unit
    25.5    val markup_command: Thy_Output.markup -> command_spec -> string ->
    25.6      (Toplevel.transition -> Toplevel.transition) parser -> unit
    25.7 -  val improper_command: command_spec -> string ->
    25.8 -    (Toplevel.transition -> Toplevel.transition) parser -> unit
    25.9    val local_theory': command_spec -> string ->
   25.10      (bool -> local_theory -> local_theory) parser -> unit
   25.11    val local_theory: command_spec -> string ->
   25.12 @@ -50,14 +48,12 @@
   25.13  datatype command = Command of
   25.14   {comment: string,
   25.15    markup: Thy_Output.markup option,
   25.16 -  int_only: bool,
   25.17    parse: (Toplevel.transition -> Toplevel.transition) parser,
   25.18    pos: Position.T,
   25.19    id: serial};
   25.20  
   25.21 -fun new_command comment markup int_only parse pos =
   25.22 -  Command {comment = comment, markup = markup, int_only = int_only, parse = parse,
   25.23 -    pos = pos, id = serial ()};
   25.24 +fun new_command comment markup parse pos =
   25.25 +  Command {comment = comment, markup = markup, parse = parse, pos = pos, id = serial ()};
   25.26  
   25.27  fun command_markup def (name, Command {pos, id, ...}) =
   25.28    Markup.properties (Position.entity_properties_of def id pos)
   25.29 @@ -153,13 +149,10 @@
   25.30    end;
   25.31  
   25.32  fun command (spec, pos) comment parse =
   25.33 -  add_command spec (new_command comment NONE false parse pos);
   25.34 +  add_command spec (new_command comment NONE parse pos);
   25.35  
   25.36  fun markup_command markup (spec, pos) comment parse =
   25.37 -  add_command spec (new_command comment (SOME markup) false parse pos);
   25.38 -
   25.39 -fun improper_command (spec, pos) comment parse =
   25.40 -  add_command spec (new_command comment NONE true parse pos);
   25.41 +  add_command spec (new_command comment (SOME markup) parse pos);
   25.42  
   25.43  end;
   25.44  
   25.45 @@ -185,14 +178,11 @@
   25.46  
   25.47  fun print_syntax () =
   25.48    let
   25.49 -    val ((keywords, _), syntax) =
   25.50 -      CRITICAL (fn () => (Keyword.dest (), #2 (get_syntax ())));
   25.51 -    val (int_cmds, cmds) =
   25.52 -      List.partition (fn (_, Command {int_only, ...}) => int_only) (dest_commands syntax);
   25.53 +    val ((keywords, _), syntax) = CRITICAL (fn () => (Keyword.dest (), #2 (get_syntax ())));
   25.54 +    val commands = dest_commands syntax;
   25.55    in
   25.56      [Pretty.strs ("syntax keywords:" :: map quote keywords),
   25.57 -      Pretty.big_list "commands:" (map pretty_command cmds),
   25.58 -      Pretty.big_list "interactive-only commands:" (map pretty_command int_cmds)]
   25.59 +      Pretty.big_list "commands:" (map pretty_command commands)]
   25.60      |> Pretty.writeln_chunks
   25.61    end;
   25.62  
   25.63 @@ -210,8 +200,7 @@
   25.64        val tr0 = Toplevel.empty |> Toplevel.name name |> Toplevel.position pos;
   25.65      in
   25.66        (case lookup_commands syntax name of
   25.67 -        SOME (Command {int_only, parse, ...}) =>
   25.68 -          Parse.!!! (Parse.tags |-- parse) >> (fn f => tr0 |> Toplevel.interactive int_only |> f)
   25.69 +        SOME (Command {parse, ...}) => Parse.!!! (Parse.tags |-- parse) >> (fn f => f tr0)
   25.70        | NONE =>
   25.71            Scan.succeed
   25.72              (tr0 |> Toplevel.imperative (fn () =>
    26.1 --- a/src/Pure/Isar/toplevel.ML	Mon Nov 03 14:31:15 2014 +0100
    26.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Nov 03 14:50:27 2014 +0100
    26.3 @@ -34,7 +34,6 @@
    26.4    val type_error: transition -> state -> string
    26.5    val name: string -> transition -> transition
    26.6    val position: Position.T -> transition -> transition
    26.7 -  val interactive: bool -> transition -> transition
    26.8    val init_theory: (unit -> theory) -> transition -> transition
    26.9    val is_init: transition -> bool
   26.10    val modify_init: (unit -> theory) -> transition -> transition
   26.11 @@ -295,18 +294,16 @@
   26.12  datatype transition = Transition of
   26.13   {name: string,              (*command name*)
   26.14    pos: Position.T,           (*source position*)
   26.15 -  int_only: bool,            (*interactive-only*)  (* TTY / Proof General legacy*)
   26.16    timing: Time.time option,  (*prescient timing information*)
   26.17    trans: trans list};        (*primitive transitions (union)*)
   26.18  
   26.19 -fun make_transition (name, pos, int_only, timing, trans) =
   26.20 -  Transition {name = name, pos = pos, int_only = int_only,
   26.21 -    timing = timing, trans = trans};
   26.22 +fun make_transition (name, pos, timing, trans) =
   26.23 +  Transition {name = name, pos = pos, timing = timing, trans = trans};
   26.24  
   26.25 -fun map_transition f (Transition {name, pos, int_only, timing, trans}) =
   26.26 -  make_transition (f (name, pos, int_only, timing, trans));
   26.27 +fun map_transition f (Transition {name, pos, timing, trans}) =
   26.28 +  make_transition (f (name, pos, timing, trans));
   26.29  
   26.30 -val empty = make_transition ("", Position.none, false, NONE, []);
   26.31 +val empty = make_transition ("", Position.none, NONE, []);
   26.32  
   26.33  
   26.34  (* diagnostics *)
   26.35 @@ -323,20 +320,17 @@
   26.36  
   26.37  (* modify transitions *)
   26.38  
   26.39 -fun name name = map_transition (fn (_, pos, int_only, timing, trans) =>
   26.40 -  (name, pos, int_only, timing, trans));
   26.41 +fun name name = map_transition (fn (_, pos, timing, trans) =>
   26.42 +  (name, pos, timing, trans));
   26.43  
   26.44 -fun position pos = map_transition (fn (name, _, int_only, timing, trans) =>
   26.45 -  (name, pos, int_only, timing, trans));
   26.46 +fun position pos = map_transition (fn (name, _, timing, trans) =>
   26.47 +  (name, pos, timing, trans));
   26.48  
   26.49 -fun interactive int_only = map_transition (fn (name, pos, _, timing, trans) =>
   26.50 -  (name, pos, int_only, timing, trans));
   26.51 +fun add_trans tr = map_transition (fn (name, pos, timing, trans) =>
   26.52 +  (name, pos, timing, tr :: trans));
   26.53  
   26.54 -fun add_trans tr = map_transition (fn (name, pos, int_only, timing, trans) =>
   26.55 -  (name, pos, int_only, timing, tr :: trans));
   26.56 -
   26.57 -val reset_trans = map_transition (fn (name, pos, int_only, timing, _) =>
   26.58 -  (name, pos, int_only, timing, []));
   26.59 +val reset_trans = map_transition (fn (name, pos, timing, _) =>
   26.60 +  (name, pos, timing, []));
   26.61  
   26.62  
   26.63  (* basic transitions *)
   26.64 @@ -559,8 +553,7 @@
   26.65  (* apply transitions *)
   26.66  
   26.67  fun get_timing (Transition {timing, ...}) = timing;
   26.68 -fun put_timing timing = map_transition (fn (name, pos, int_only, _, trans) =>
   26.69 -  (name, pos, int_only, timing, trans));
   26.70 +fun put_timing timing = map_transition (fn (name, pos, _, trans) => (name, pos, timing, trans));
   26.71  
   26.72  local
   26.73  
    27.1 --- a/src/Pure/Tools/class_deps.ML	Mon Nov 03 14:31:15 2014 +0100
    27.2 +++ b/src/Pure/Tools/class_deps.ML	Mon Nov 03 14:50:27 2014 +0100
    27.3 @@ -37,7 +37,7 @@
    27.4  val visualize_cmd = gen_visualize Syntax.read_sort;
    27.5  
    27.6  val _ =
    27.7 -  Outer_Syntax.improper_command @{command_spec "class_deps"} "visualize class dependencies"
    27.8 +  Outer_Syntax.command @{command_spec "class_deps"} "visualize class dependencies"
    27.9      ((Scan.optional Parse.sort "{}" -- Scan.option Parse.sort) >> (fn (raw_super, raw_sub) =>
   27.10        ((Toplevel.unknown_theory oo Toplevel.keep) (fn st => visualize_cmd (Toplevel.context_of st) raw_super raw_sub))));
   27.11  
    28.1 --- a/src/Pure/Tools/find_consts.ML	Mon Nov 03 14:31:15 2014 +0100
    28.2 +++ b/src/Pure/Tools/find_consts.ML	Mon Nov 03 14:50:27 2014 +0100
    28.3 @@ -149,7 +149,7 @@
    28.4    |> #1;
    28.5  
    28.6  val _ =
    28.7 -  Outer_Syntax.improper_command @{command_spec "find_consts"}
    28.8 +  Outer_Syntax.command @{command_spec "find_consts"}
    28.9      "find constants by name / type patterns"
   28.10      (query >> (fn spec =>
   28.11        Toplevel.keep (fn st =>
    29.1 --- a/src/Pure/Tools/find_theorems.ML	Mon Nov 03 14:31:15 2014 +0100
    29.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon Nov 03 14:50:27 2014 +0100
    29.3 @@ -535,7 +535,7 @@
    29.4    |> #1;
    29.5  
    29.6  val _ =
    29.7 -  Outer_Syntax.improper_command @{command_spec "find_theorems"}
    29.8 +  Outer_Syntax.command @{command_spec "find_theorems"}
    29.9      "find theorems meeting specified criteria"
   29.10      (options -- query >> (fn ((opt_lim, rem_dups), spec) =>
   29.11        Toplevel.keep (fn st =>
    30.1 --- a/src/Pure/Tools/thm_deps.ML	Mon Nov 03 14:31:15 2014 +0100
    30.2 +++ b/src/Pure/Tools/thm_deps.ML	Mon Nov 03 14:50:27 2014 +0100
    30.3 @@ -45,7 +45,7 @@
    30.4    in Graph_Display.display_graph (sort_wrt #ID deps) end;
    30.5  
    30.6  val _ =
    30.7 -  Outer_Syntax.improper_command @{command_spec "thm_deps"} "visualize theorem dependencies"
    30.8 +  Outer_Syntax.command @{command_spec "thm_deps"} "visualize theorem dependencies"
    30.9      (Parse.xthms1 >> (fn args =>
   30.10        Toplevel.unknown_theory o Toplevel.keep (fn state =>
   30.11          thm_deps (Toplevel.theory_of state) (Attrib.eval_thms (Toplevel.context_of state) args))));
   30.12 @@ -102,7 +102,7 @@
   30.13    in rev thms' end;
   30.14  
   30.15  val _ =
   30.16 -  Outer_Syntax.improper_command @{command_spec "unused_thms"} "find unused theorems"
   30.17 +  Outer_Syntax.command @{command_spec "unused_thms"} "find unused theorems"
   30.18      (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
   30.19         Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >> (fn opt_range =>
   30.20          Toplevel.keep (fn state =>
    31.1 --- a/src/Tools/Code/code_preproc.ML	Mon Nov 03 14:31:15 2014 +0100
    31.2 +++ b/src/Tools/Code/code_preproc.ML	Mon Nov 03 14:50:27 2014 +0100
    31.3 @@ -584,7 +584,7 @@
    31.4    end;
    31.5  
    31.6  val _ =
    31.7 -  Outer_Syntax.improper_command @{command_spec "print_codeproc"} "print code preprocessor setup"
    31.8 +  Outer_Syntax.command @{command_spec "print_codeproc"} "print code preprocessor setup"
    31.9      (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_codeproc o Toplevel.context_of)));
   31.10  
   31.11  end; (*struct*)
    32.1 --- a/src/Tools/Code/code_thingol.ML	Mon Nov 03 14:31:15 2014 +0100
    32.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Nov 03 14:50:27 2014 +0100
    32.3 @@ -939,14 +939,14 @@
    32.4  in
    32.5  
    32.6  val _ =
    32.7 -  Outer_Syntax.improper_command @{command_spec "code_thms"}
    32.8 +  Outer_Syntax.command @{command_spec "code_thms"}
    32.9      "print system of code equations for code"
   32.10      (Scan.repeat1 Parse.term >> (fn cs =>
   32.11        Toplevel.unknown_context o
   32.12        Toplevel.keep (fn state => code_thms_cmd (Toplevel.context_of state) cs)));
   32.13  
   32.14  val _ =
   32.15 -  Outer_Syntax.improper_command @{command_spec "code_deps"}
   32.16 +  Outer_Syntax.command @{command_spec "code_deps"}
   32.17      "visualize dependencies of code equations for code"
   32.18      (Scan.repeat1 Parse.term >> (fn cs =>
   32.19        Toplevel.unknown_context o
    33.1 --- a/src/Tools/induct.ML	Mon Nov 03 14:31:15 2014 +0100
    33.2 +++ b/src/Tools/induct.ML	Mon Nov 03 14:50:27 2014 +0100
    33.3 @@ -257,7 +257,7 @@
    33.4    end;
    33.5  
    33.6  val _ =
    33.7 -  Outer_Syntax.improper_command @{command_spec "print_induct_rules"}
    33.8 +  Outer_Syntax.command @{command_spec "print_induct_rules"}
    33.9      "print induction and cases rules"
   33.10      (Scan.succeed (Toplevel.unknown_context o
   33.11        Toplevel.keep (print_rules o Toplevel.context_of)));
    34.1 --- a/src/Tools/quickcheck.ML	Mon Nov 03 14:31:15 2014 +0100
    34.2 +++ b/src/Tools/quickcheck.ML	Mon Nov 03 14:50:27 2014 +0100
    34.3 @@ -534,7 +534,7 @@
    34.4      (parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args)));
    34.5  
    34.6  val _ =
    34.7 -  Outer_Syntax.improper_command @{command_spec "quickcheck"}
    34.8 +  Outer_Syntax.command @{command_spec "quickcheck"}
    34.9      "try to find counterexample for subgoal"
   34.10      (parse_args -- Scan.optional Parse.nat 1 >> (fn (args, i) =>
   34.11        Toplevel.unknown_proof o Toplevel.keep (quickcheck_cmd args i)));
    35.1 --- a/src/Tools/solve_direct.ML	Mon Nov 03 14:31:15 2014 +0100
    35.2 +++ b/src/Tools/solve_direct.ML	Mon Nov 03 14:50:27 2014 +0100
    35.3 @@ -93,7 +93,7 @@
    35.4  val solve_direct = do_solve_direct Normal
    35.5  
    35.6  val _ =
    35.7 -  Outer_Syntax.improper_command @{command_spec "solve_direct"}
    35.8 +  Outer_Syntax.command @{command_spec "solve_direct"}
    35.9      "try to solve conjectures directly with existing theorems"
   35.10      (Scan.succeed (Toplevel.unknown_proof o
   35.11        Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
    36.1 --- a/src/Tools/subtyping.ML	Mon Nov 03 14:31:15 2014 +0100
    36.2 +++ b/src/Tools/subtyping.ML	Mon Nov 03 14:50:27 2014 +0100
    36.3 @@ -1114,7 +1114,7 @@
    36.4  (* outer syntax commands *)
    36.5  
    36.6  val _ =
    36.7 -  Outer_Syntax.improper_command @{command_spec "print_coercions"}
    36.8 +  Outer_Syntax.command @{command_spec "print_coercions"}
    36.9      "print information about coercions"
   36.10      (Scan.succeed (Toplevel.keep (print_coercions o Toplevel.context_of)));
   36.11  
    37.1 --- a/src/Tools/try.ML	Mon Nov 03 14:31:15 2014 +0100
    37.2 +++ b/src/Tools/try.ML	Mon Nov 03 14:50:27 2014 +0100
    37.3 @@ -75,7 +75,7 @@
    37.4      |> tap (fn NONE => writeln "Tried in vain." | _ => ())
    37.5  
    37.6  val _ =
    37.7 -  Outer_Syntax.improper_command @{command_spec "try"}
    37.8 +  Outer_Syntax.command @{command_spec "try"}
    37.9      "try a combination of automatic proving and disproving tools"
   37.10      (Scan.succeed (Toplevel.unknown_proof o Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
   37.11  
    38.1 --- a/src/ZF/Tools/typechk.ML	Mon Nov 03 14:31:15 2014 +0100
    38.2 +++ b/src/ZF/Tools/typechk.ML	Mon Nov 03 14:50:27 2014 +0100
    38.3 @@ -125,7 +125,7 @@
    38.4        "ZF type-checking");
    38.5  
    38.6  val _ =
    38.7 -  Outer_Syntax.improper_command @{command_spec "print_tcset"} "print context of ZF typecheck"
    38.8 +  Outer_Syntax.command @{command_spec "print_tcset"} "print context of ZF typecheck"
    38.9      (Scan.succeed (Toplevel.unknown_context o
   38.10        Toplevel.keep (print_tcset o Toplevel.context_of)));
   38.11