# HG changeset patch
# User wenzelm
# Date 1415022627 -3600
# Node ID 9e0ecb66d6a74204beee23509ddb9c30ffd33f51
# Parent  20aa19ecf2cc540d81adfbd503b4993aa48253bb
eliminated unused int_only flag (see also c12484a27367);
just proper commands;

diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/HOL/Decision_Procs/approximation.ML
--- a/src/HOL/Decision_Procs/approximation.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Decision_Procs/approximation.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -151,7 +151,7 @@
   Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "approximate"} "print approximation of term"
+  Outer_Syntax.command @{command_spec "approximate"} "print approximation of term"
     (opt_modes -- Parse.term
       >> (fn (modes, t) => Toplevel.keep (approximate_cmd modes t)));
 
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/HOL/Library/Old_SMT/old_smt_config.ML
--- a/src/HOL/Library/Old_SMT/old_smt_config.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Library/Old_SMT/old_smt_config.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -246,7 +246,7 @@
   end
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "old_smt_status"}
+  Outer_Syntax.command @{command_spec "old_smt_status"}
     "show the available SMT solvers, the currently selected SMT solver, \
     \and the values of SMT configuration options"
     (Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of)))
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/HOL/Library/refute.ML
--- a/src/HOL/Library/refute.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Library/refute.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -2967,7 +2967,7 @@
 (* 'refute' command *)
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "refute"}
+  Outer_Syntax.command @{command_spec "refute"}
     "try to find a model that refutes a given subgoal"
     (scan_parms -- Scan.optional Parse.nat 1 >>
       (fn (parms, i) =>
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Orderings.thy	Mon Nov 03 14:50:27 2014 +0100
@@ -439,7 +439,7 @@
   end;
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_orders"}
+  Outer_Syntax.command @{command_spec "print_orders"}
     "print order structures available to transitivity reasoner"
     (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (print_structures o Toplevel.context_of)));
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -126,7 +126,7 @@
     (Parse.name >> (fn name => Toplevel.local_theory_to_proof NONE (prove_vc name)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "spark_status"}
+  Outer_Syntax.command @{command_spec "spark_status"}
     "show the name and state of all loaded verification conditions"
     (Scan.optional
        (Args.parens
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -912,7 +912,7 @@
   in TPTP_Data.map (cons ((prob_name, result))) thy' end
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "import_tptp"} "import TPTP problem"
+  Outer_Syntax.command @{command_spec "import_tptp"} "import TPTP problem"
     (Parse.path >> (fn name =>
       Toplevel.theory (fn thy =>
         let val path = Path.explode name
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -1866,7 +1866,7 @@
 
 (*This has been disabled since it requires a hook to be specified to use "import_thm"
 val _ =
-  Outer_Syntax.improper_command @{command_spec "import_leo2_proof"} "import TPTP proof"
+  Outer_Syntax.command @{command_spec "import_leo2_proof"} "import TPTP proof"
     (Parse.path >> (fn name =>
       Toplevel.theory (fn thy =>
        let val path = Path.explode name
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -1598,7 +1598,7 @@
   end;
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_bnfs"}
+  Outer_Syntax.command @{command_spec "print_bnfs"}
     "print all bounded natural functors"
     (Scan.succeed (Toplevel.keep (print_bnfs o Toplevel.context_of)));
 
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/HOL/Tools/Ctr_Sugar/case_translation.ML
--- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -630,7 +630,7 @@
   end;
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_case_translations"}
+  Outer_Syntax.command @{command_spec "print_case_translations"}
     "print registered case combinators and constructors"
     (Scan.succeed (Toplevel.keep (print_case_translations o Toplevel.context_of)))
 
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/HOL/Tools/Lifting/lifting_info.ML
--- a/src/HOL/Tools/Lifting/lifting_info.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_info.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -532,11 +532,11 @@
 (* outer syntax commands *)
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_quot_maps"} "print quotient map functions"
+  Outer_Syntax.command @{command_spec "print_quot_maps"} "print quotient map functions"
     (Scan.succeed (Toplevel.keep (print_quot_maps o Toplevel.context_of)))
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_quotients"} "print quotients"
+  Outer_Syntax.command @{command_spec "print_quotients"} "print quotients"
     (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
 
 end
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/HOL/Tools/Nitpick/nitpick_commands.ML
--- a/src/HOL/Tools/Nitpick/nitpick_commands.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -374,7 +374,7 @@
                                       |> sort_strings |> cat_lines)))))
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "nitpick"}
+  Outer_Syntax.command @{command_spec "nitpick"}
     "try to find a counterexample for a given subgoal using Nitpick"
     (parse_params -- Scan.optional Parse.nat 1 >> (fn (params, i) =>
       Toplevel.unknown_proof o
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -1028,7 +1028,7 @@
   Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "values_prolog"}
+  Outer_Syntax.command @{command_spec "values_prolog"}
     "enumerate and print comprehensions"
     (opt_print_modes -- Scan.optional (Parse.nat >> SOME) NONE -- Parse.term
      >> (fn ((print_modes, soln), t) => Toplevel.keep (values_cmd print_modes soln t)))
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -287,7 +287,7 @@
     (opt_expected_modes -- opt_modes -- scan_options -- Parse.term >> code_pred_cmd)
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "values"}
+  Outer_Syntax.command @{command_spec "values"}
     "enumerate and print comprehensions"
     (opt_print_modes -- opt_param_modes -- value_options -- Scan.optional Parse.nat ~1 -- Parse.term
       >> (fn ((((print_modes, param_modes), options), k), t) => Toplevel.keep
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/HOL/Tools/Quickcheck/find_unused_assms.ML
--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -111,7 +111,7 @@
 end
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "find_unused_assms"}
+  Outer_Syntax.command @{command_spec "find_unused_assms"}
     "find theorems with (potentially) superfluous assumptions"
     (Scan.option Parse.name >> (fn name =>
       Toplevel.keep (fn state => print_unused_assms (Toplevel.context_of state) name)))
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/HOL/Tools/Quotient/quotient_info.ML
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -229,15 +229,15 @@
 (* outer syntax commands *)
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_quotmapsQ3"} "print quotient map functions"
+  Outer_Syntax.command @{command_spec "print_quotmapsQ3"} "print quotient map functions"
     (Scan.succeed (Toplevel.keep (print_quotmaps o Toplevel.context_of)))
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_quotientsQ3"} "print quotients"
+  Outer_Syntax.command @{command_spec "print_quotientsQ3"} "print quotients"
     (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_quotconsts"} "print quotient constants"
+  Outer_Syntax.command @{command_spec "print_quotconsts"} "print quotient constants"
     (Scan.succeed (Toplevel.keep (print_quotconsts o Toplevel.context_of)))
 
 end;
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -241,7 +241,7 @@
   end
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "smt_status"}
+  Outer_Syntax.command @{command_spec "smt_status"}
     "show the available SMT solvers, the currently selected SMT solver, \
     \and the values of SMT configuration options"
     (Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of)))
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -386,7 +386,7 @@
     no_fact_override
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "sledgehammer"}
+  Outer_Syntax.command @{command_spec "sledgehammer"}
     "search for first-order proof using automatic theorem provers"
     ((Scan.optional Parse.name runN -- parse_params
       -- parse_fact_override -- Scan.option Parse.nat) #>> sledgehammer_trans)
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Tools/inductive.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -1179,7 +1179,7 @@
     (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_simps));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_inductives"}
+  Outer_Syntax.command @{command_spec "print_inductives"}
     "print (co)inductive definitions and monotonicity rules"
     (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (print_inductives o Toplevel.context_of)));
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Tools/try0.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -180,7 +180,7 @@
    || Scan.repeat parse_attr >> (fn quad => fold merge_attrs quad ([], [], [], []))) x;
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "try0"} "try a combination of proof methods"
+  Outer_Syntax.command @{command_spec "try0"} "try a combination of proof methods"
     (Scan.optional parse_attrs ([], [], [], []) #>> try0_trans);
 
 fun try_try0 auto = generic_try0 (if auto then Auto_Try else Try) NONE ([], [], [], []);
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/HOL/Tools/value.ML
--- a/src/HOL/Tools/value.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Tools/value.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -70,7 +70,7 @@
   Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"})
   
 val _ =
-  Outer_Syntax.improper_command @{command_spec "value"} "evaluate and print term"
+  Outer_Syntax.command @{command_spec "value"} "evaluate and print term"
     (opt_evaluator -- opt_modes -- Parse.term
       >> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t)));
 
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy	Mon Nov 03 14:50:27 2014 +0100
@@ -36,7 +36,7 @@
 subsection {* Outer syntax: cartouche within command syntax *}
 
 ML {*
-  Outer_Syntax.improper_command @{command_spec "cartouche"} ""
+  Outer_Syntax.command @{command_spec "cartouche"} ""
     (Parse.cartouche >> (fn s =>
       Toplevel.imperative (fn () => writeln s)))
 *}
@@ -112,7 +112,7 @@
 subsubsection {* Term cartouche and regular quotes *}
 
 ML {*
-  Outer_Syntax.improper_command @{command_spec "term_cartouche"} ""
+  Outer_Syntax.command @{command_spec "term_cartouche"} ""
     (Parse.inner_syntax Parse.cartouche >> (fn s =>
       Toplevel.keep (fn state =>
         let
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Provers/classical.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -980,7 +980,7 @@
 (** outer syntax **)
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_claset"} "print context of Classical Reasoner"
+  Outer_Syntax.command @{command_spec "print_claset"} "print context of Classical Reasoner"
     (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_claset o Toplevel.context_of)));
 
 end;
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Pure/Isar/calculation.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -222,7 +222,7 @@
     (Scan.succeed (Toplevel.proof' ultimately));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_trans_rules"} "print transitivity rules"
+  Outer_Syntax.command @{command_spec "print_trans_rules"} "print transitivity rules"
     (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_rules o Toplevel.context_of)));
 
 end;
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -397,7 +397,7 @@
     (Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.including_cmd));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_bundles"}
+  Outer_Syntax.command @{command_spec "print_bundles"}
     "print bundles of declarations"
     (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Bundle.print_bundles o Toplevel.context_of)));
@@ -727,194 +727,194 @@
 val opt_bang = Scan.optional (@{keyword "!"} >> K true) false;
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "help"}
+  Outer_Syntax.command @{command_spec "help"}
     "retrieve outer syntax commands according to name patterns"
     (Scan.repeat Parse.name >>
       (fn pats => Toplevel.imperative (fn () => Outer_Syntax.help_syntax pats)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_commands"} "print outer syntax commands"
+  Outer_Syntax.command @{command_spec "print_commands"} "print outer syntax commands"
     (Scan.succeed (Toplevel.imperative Outer_Syntax.print_syntax));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_options"} "print configuration options"
+  Outer_Syntax.command @{command_spec "print_options"} "print configuration options"
     (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Attrib.print_options o Toplevel.context_of)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_context"}
+  Outer_Syntax.command @{command_spec "print_context"}
     "print context of local theory target"
     (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_context)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_theory"}
+  Outer_Syntax.command @{command_spec "print_theory"}
     "print logical theory contents (verbose!)"
     (opt_bang >> (fn b => Toplevel.unknown_theory o
       Toplevel.keep (Pretty.writeln o Proof_Display.pretty_full_theory b o Toplevel.theory_of)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_syntax"}
+  Outer_Syntax.command @{command_spec "print_syntax"}
     "print inner syntax of context (verbose!)"
     (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_defn_rules"}
+  Outer_Syntax.command @{command_spec "print_defn_rules"}
     "print definitional rewrite rules of context"
     (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_abbrevs"}
+  Outer_Syntax.command @{command_spec "print_abbrevs"}
     "print constant abbreviations of context"
     (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Proof_Context.print_abbrevs o Toplevel.context_of)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_theorems"}
+  Outer_Syntax.command @{command_spec "print_theorems"}
     "print theorems of local theory or proof context"
     (opt_bang >> (fn b =>
       Toplevel.unknown_context o
       Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_locales"}
+  Outer_Syntax.command @{command_spec "print_locales"}
     "print locales of this theory"
     (Scan.succeed (Toplevel.unknown_theory o
       Toplevel.keep (Locale.print_locales o Toplevel.theory_of)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_classes"}
+  Outer_Syntax.command @{command_spec "print_classes"}
     "print classes of this theory"
     (Scan.succeed (Toplevel.unknown_theory o
       Toplevel.keep (Class.print_classes o Toplevel.context_of)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_locale"}
+  Outer_Syntax.command @{command_spec "print_locale"}
     "print locale of this theory"
     (opt_bang -- Parse.position Parse.xname >> (fn (b, name) =>
       Toplevel.unknown_theory o
       Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_interps"}
+  Outer_Syntax.command @{command_spec "print_interps"}
     "print interpretations of locale for this theory or proof context"
     (Parse.position Parse.xname >> (fn name =>
       Toplevel.unknown_context o
       Toplevel.keep (fn state => Locale.print_registrations (Toplevel.context_of state) name)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_dependencies"}
+  Outer_Syntax.command @{command_spec "print_dependencies"}
     "print dependencies of locale expression"
     (opt_bang -- Parse_Spec.locale_expression true >> (fn (b, expr) =>
       Toplevel.unknown_context o
       Toplevel.keep (fn state => Expression.print_dependencies (Toplevel.context_of state) b expr)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_attributes"}
+  Outer_Syntax.command @{command_spec "print_attributes"}
     "print attributes of this theory"
     (Scan.succeed (Toplevel.unknown_theory o
       Toplevel.keep (Attrib.print_attributes o Toplevel.context_of)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_simpset"}
+  Outer_Syntax.command @{command_spec "print_simpset"}
     "print context of Simplifier"
     (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset o Toplevel.context_of)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_rules"} "print intro/elim rules"
+  Outer_Syntax.command @{command_spec "print_rules"} "print intro/elim rules"
     (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_methods"} "print methods of this theory"
+  Outer_Syntax.command @{command_spec "print_methods"} "print methods of this theory"
     (Scan.succeed (Toplevel.unknown_theory o
       Toplevel.keep (Method.print_methods o Toplevel.context_of)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_antiquotations"}
+  Outer_Syntax.command @{command_spec "print_antiquotations"}
     "print document antiquotations"
     (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Thy_Output.print_antiquotations o Toplevel.context_of)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_ML_antiquotations"}
+  Outer_Syntax.command @{command_spec "print_ML_antiquotations"}
     "print ML antiquotations"
     (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (ML_Context.print_antiquotations o Toplevel.context_of)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "thy_deps"} "visualize theory dependencies"
+  Outer_Syntax.command @{command_spec "thy_deps"} "visualize theory dependencies"
     (Scan.succeed Isar_Cmd.thy_deps);
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "locale_deps"} "visualize locale dependencies"
+  Outer_Syntax.command @{command_spec "locale_deps"} "visualize locale dependencies"
     (Scan.succeed Isar_Cmd.locale_deps);
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_term_bindings"}
+  Outer_Syntax.command @{command_spec "print_term_bindings"}
     "print term bindings of proof context"
     (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep
         (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_facts"} "print facts of proof context"
+  Outer_Syntax.command @{command_spec "print_facts"} "print facts of proof context"
     (opt_bang >> (fn verbose => Toplevel.unknown_context o
       Toplevel.keep (fn st => Proof_Context.print_local_facts (Toplevel.context_of st) verbose)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_cases"} "print cases of proof context"
+  Outer_Syntax.command @{command_spec "print_cases"} "print cases of proof context"
     (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_statement"}
+  Outer_Syntax.command @{command_spec "print_statement"}
     "print theorems as long statements"
     (opt_modes -- Parse.xthms1 >> Isar_Cmd.print_stmts);
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "thm"} "print theorems"
+  Outer_Syntax.command @{command_spec "thm"} "print theorems"
     (opt_modes -- Parse.xthms1 >> Isar_Cmd.print_thms);
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "prf"} "print proof terms of theorems"
+  Outer_Syntax.command @{command_spec "prf"} "print proof terms of theorems"
     (opt_modes -- Scan.option Parse.xthms1 >> Isar_Cmd.print_prfs false);
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "full_prf"} "print full proof terms of theorems"
+  Outer_Syntax.command @{command_spec "full_prf"} "print full proof terms of theorems"
     (opt_modes -- Scan.option Parse.xthms1 >> Isar_Cmd.print_prfs true);
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "prop"} "read and print proposition"
+  Outer_Syntax.command @{command_spec "prop"} "read and print proposition"
     (opt_modes -- Parse.term >> Isar_Cmd.print_prop);
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "term"} "read and print term"
+  Outer_Syntax.command @{command_spec "term"} "read and print term"
     (opt_modes -- Parse.term >> Isar_Cmd.print_term);
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "typ"} "read and print type"
+  Outer_Syntax.command @{command_spec "typ"} "read and print type"
     (opt_modes -- (Parse.typ -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort))
       >> Isar_Cmd.print_type);
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_codesetup"} "print code generator setup"
+  Outer_Syntax.command @{command_spec "print_codesetup"} "print code generator setup"
     (Scan.succeed (Toplevel.unknown_theory o
       Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_state"}
+  Outer_Syntax.command @{command_spec "print_state"}
     "print current proof state (if present)"
     (opt_modes >> (fn modes => Toplevel.keep (Print_Mode.with_modes modes Toplevel.print_state)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "welcome"} "print welcome message"
+  Outer_Syntax.command @{command_spec "welcome"} "print welcome message"
     (Scan.succeed (Toplevel.imperative (writeln o Session.welcome)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "display_drafts"}
+  Outer_Syntax.command @{command_spec "display_drafts"}
     "display raw source files with symbols"
     (Scan.repeat1 Parse.path >> (fn names =>
       Toplevel.imperative (fn () => ignore (Present.display_drafts (map Path.explode names)))));
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -19,8 +19,6 @@
     (Toplevel.transition -> Toplevel.transition) parser -> unit
   val markup_command: Thy_Output.markup -> command_spec -> string ->
     (Toplevel.transition -> Toplevel.transition) parser -> unit
-  val improper_command: command_spec -> string ->
-    (Toplevel.transition -> Toplevel.transition) parser -> unit
   val local_theory': command_spec -> string ->
     (bool -> local_theory -> local_theory) parser -> unit
   val local_theory: command_spec -> string ->
@@ -50,14 +48,12 @@
 datatype command = Command of
  {comment: string,
   markup: Thy_Output.markup option,
-  int_only: bool,
   parse: (Toplevel.transition -> Toplevel.transition) parser,
   pos: Position.T,
   id: serial};
 
-fun new_command comment markup int_only parse pos =
-  Command {comment = comment, markup = markup, int_only = int_only, parse = parse,
-    pos = pos, id = serial ()};
+fun new_command comment markup parse pos =
+  Command {comment = comment, markup = markup, parse = parse, pos = pos, id = serial ()};
 
 fun command_markup def (name, Command {pos, id, ...}) =
   Markup.properties (Position.entity_properties_of def id pos)
@@ -153,13 +149,10 @@
   end;
 
 fun command (spec, pos) comment parse =
-  add_command spec (new_command comment NONE false parse pos);
+  add_command spec (new_command comment NONE parse pos);
 
 fun markup_command markup (spec, pos) comment parse =
-  add_command spec (new_command comment (SOME markup) false parse pos);
-
-fun improper_command (spec, pos) comment parse =
-  add_command spec (new_command comment NONE true parse pos);
+  add_command spec (new_command comment (SOME markup) parse pos);
 
 end;
 
@@ -185,14 +178,11 @@
 
 fun print_syntax () =
   let
-    val ((keywords, _), syntax) =
-      CRITICAL (fn () => (Keyword.dest (), #2 (get_syntax ())));
-    val (int_cmds, cmds) =
-      List.partition (fn (_, Command {int_only, ...}) => int_only) (dest_commands syntax);
+    val ((keywords, _), syntax) = CRITICAL (fn () => (Keyword.dest (), #2 (get_syntax ())));
+    val commands = dest_commands syntax;
   in
     [Pretty.strs ("syntax keywords:" :: map quote keywords),
-      Pretty.big_list "commands:" (map pretty_command cmds),
-      Pretty.big_list "interactive-only commands:" (map pretty_command int_cmds)]
+      Pretty.big_list "commands:" (map pretty_command commands)]
     |> Pretty.writeln_chunks
   end;
 
@@ -210,8 +200,7 @@
       val tr0 = Toplevel.empty |> Toplevel.name name |> Toplevel.position pos;
     in
       (case lookup_commands syntax name of
-        SOME (Command {int_only, parse, ...}) =>
-          Parse.!!! (Parse.tags |-- parse) >> (fn f => tr0 |> Toplevel.interactive int_only |> f)
+        SOME (Command {parse, ...}) => Parse.!!! (Parse.tags |-- parse) >> (fn f => f tr0)
       | NONE =>
           Scan.succeed
             (tr0 |> Toplevel.imperative (fn () =>
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Pure/Isar/toplevel.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -34,7 +34,6 @@
   val type_error: transition -> state -> string
   val name: string -> transition -> transition
   val position: Position.T -> transition -> transition
-  val interactive: bool -> transition -> transition
   val init_theory: (unit -> theory) -> transition -> transition
   val is_init: transition -> bool
   val modify_init: (unit -> theory) -> transition -> transition
@@ -295,18 +294,16 @@
 datatype transition = Transition of
  {name: string,              (*command name*)
   pos: Position.T,           (*source position*)
-  int_only: bool,            (*interactive-only*)  (* TTY / Proof General legacy*)
   timing: Time.time option,  (*prescient timing information*)
   trans: trans list};        (*primitive transitions (union)*)
 
-fun make_transition (name, pos, int_only, timing, trans) =
-  Transition {name = name, pos = pos, int_only = int_only,
-    timing = timing, trans = trans};
+fun make_transition (name, pos, timing, trans) =
+  Transition {name = name, pos = pos, timing = timing, trans = trans};
 
-fun map_transition f (Transition {name, pos, int_only, timing, trans}) =
-  make_transition (f (name, pos, int_only, timing, trans));
+fun map_transition f (Transition {name, pos, timing, trans}) =
+  make_transition (f (name, pos, timing, trans));
 
-val empty = make_transition ("", Position.none, false, NONE, []);
+val empty = make_transition ("", Position.none, NONE, []);
 
 
 (* diagnostics *)
@@ -323,20 +320,17 @@
 
 (* modify transitions *)
 
-fun name name = map_transition (fn (_, pos, int_only, timing, trans) =>
-  (name, pos, int_only, timing, trans));
+fun name name = map_transition (fn (_, pos, timing, trans) =>
+  (name, pos, timing, trans));
 
-fun position pos = map_transition (fn (name, _, int_only, timing, trans) =>
-  (name, pos, int_only, timing, trans));
+fun position pos = map_transition (fn (name, _, timing, trans) =>
+  (name, pos, timing, trans));
 
-fun interactive int_only = map_transition (fn (name, pos, _, timing, trans) =>
-  (name, pos, int_only, timing, trans));
+fun add_trans tr = map_transition (fn (name, pos, timing, trans) =>
+  (name, pos, timing, tr :: trans));
 
-fun add_trans tr = map_transition (fn (name, pos, int_only, timing, trans) =>
-  (name, pos, int_only, timing, tr :: trans));
-
-val reset_trans = map_transition (fn (name, pos, int_only, timing, _) =>
-  (name, pos, int_only, timing, []));
+val reset_trans = map_transition (fn (name, pos, timing, _) =>
+  (name, pos, timing, []));
 
 
 (* basic transitions *)
@@ -559,8 +553,7 @@
 (* apply transitions *)
 
 fun get_timing (Transition {timing, ...}) = timing;
-fun put_timing timing = map_transition (fn (name, pos, int_only, _, trans) =>
-  (name, pos, int_only, timing, trans));
+fun put_timing timing = map_transition (fn (name, pos, _, trans) => (name, pos, timing, trans));
 
 local
 
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/Pure/Tools/class_deps.ML
--- a/src/Pure/Tools/class_deps.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Pure/Tools/class_deps.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -37,7 +37,7 @@
 val visualize_cmd = gen_visualize Syntax.read_sort;
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "class_deps"} "visualize class dependencies"
+  Outer_Syntax.command @{command_spec "class_deps"} "visualize class dependencies"
     ((Scan.optional Parse.sort "{}" -- Scan.option Parse.sort) >> (fn (raw_super, raw_sub) =>
       ((Toplevel.unknown_theory oo Toplevel.keep) (fn st => visualize_cmd (Toplevel.context_of st) raw_super raw_sub))));
 
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Pure/Tools/find_consts.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -149,7 +149,7 @@
   |> #1;
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "find_consts"}
+  Outer_Syntax.command @{command_spec "find_consts"}
     "find constants by name / type patterns"
     (query >> (fn spec =>
       Toplevel.keep (fn st =>
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -535,7 +535,7 @@
   |> #1;
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "find_theorems"}
+  Outer_Syntax.command @{command_spec "find_theorems"}
     "find theorems meeting specified criteria"
     (options -- query >> (fn ((opt_lim, rem_dups), spec) =>
       Toplevel.keep (fn st =>
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/Pure/Tools/thm_deps.ML
--- a/src/Pure/Tools/thm_deps.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Pure/Tools/thm_deps.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -45,7 +45,7 @@
   in Graph_Display.display_graph (sort_wrt #ID deps) end;
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "thm_deps"} "visualize theorem dependencies"
+  Outer_Syntax.command @{command_spec "thm_deps"} "visualize theorem dependencies"
     (Parse.xthms1 >> (fn args =>
       Toplevel.unknown_theory o Toplevel.keep (fn state =>
         thm_deps (Toplevel.theory_of state) (Attrib.eval_thms (Toplevel.context_of state) args))));
@@ -102,7 +102,7 @@
   in rev thms' end;
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "unused_thms"} "find unused theorems"
+  Outer_Syntax.command @{command_spec "unused_thms"} "find unused theorems"
     (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
        Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >> (fn opt_range =>
         Toplevel.keep (fn state =>
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Tools/Code/code_preproc.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -584,7 +584,7 @@
   end;
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_codeproc"} "print code preprocessor setup"
+  Outer_Syntax.command @{command_spec "print_codeproc"} "print code preprocessor setup"
     (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_codeproc o Toplevel.context_of)));
 
 end; (*struct*)
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Tools/Code/code_thingol.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -939,14 +939,14 @@
 in
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "code_thms"}
+  Outer_Syntax.command @{command_spec "code_thms"}
     "print system of code equations for code"
     (Scan.repeat1 Parse.term >> (fn cs =>
       Toplevel.unknown_context o
       Toplevel.keep (fn state => code_thms_cmd (Toplevel.context_of state) cs)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "code_deps"}
+  Outer_Syntax.command @{command_spec "code_deps"}
     "visualize dependencies of code equations for code"
     (Scan.repeat1 Parse.term >> (fn cs =>
       Toplevel.unknown_context o
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Tools/induct.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -257,7 +257,7 @@
   end;
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_induct_rules"}
+  Outer_Syntax.command @{command_spec "print_induct_rules"}
     "print induction and cases rules"
     (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (print_rules o Toplevel.context_of)));
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Tools/quickcheck.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -534,7 +534,7 @@
     (parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "quickcheck"}
+  Outer_Syntax.command @{command_spec "quickcheck"}
     "try to find counterexample for subgoal"
     (parse_args -- Scan.optional Parse.nat 1 >> (fn (args, i) =>
       Toplevel.unknown_proof o Toplevel.keep (quickcheck_cmd args i)));
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/Tools/solve_direct.ML
--- a/src/Tools/solve_direct.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Tools/solve_direct.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -93,7 +93,7 @@
 val solve_direct = do_solve_direct Normal
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "solve_direct"}
+  Outer_Syntax.command @{command_spec "solve_direct"}
     "try to solve conjectures directly with existing theorems"
     (Scan.succeed (Toplevel.unknown_proof o
       Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Tools/subtyping.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -1114,7 +1114,7 @@
 (* outer syntax commands *)
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_coercions"}
+  Outer_Syntax.command @{command_spec "print_coercions"}
     "print information about coercions"
     (Scan.succeed (Toplevel.keep (print_coercions o Toplevel.context_of)));
 
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/Tools/try.ML
--- a/src/Tools/try.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Tools/try.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -75,7 +75,7 @@
     |> tap (fn NONE => writeln "Tried in vain." | _ => ())
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "try"}
+  Outer_Syntax.command @{command_spec "try"}
     "try a combination of automatic proving and disproving tools"
     (Scan.succeed (Toplevel.unknown_proof o Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
 
diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/ZF/Tools/typechk.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -125,7 +125,7 @@
       "ZF type-checking");
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_tcset"} "print context of ZF typecheck"
+  Outer_Syntax.command @{command_spec "print_tcset"} "print context of ZF typecheck"
     (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (print_tcset o Toplevel.context_of)));