# HG changeset patch
# User blanchet
# Date 1269267798 -3600
# Node ID 0e2d57686b3ce9bc7a7346570190f6e4d8946797
# Parent  02595d4a3a7c48eaf110b498d3bea8dc79c0919f
make "sledgehammer" and "atp_minimize" improper commands

diff -r 02595d4a3a7c -r 0e2d57686b3c src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Mar 22 15:07:07 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Mar 22 15:23:18 2010 +0100
@@ -31,7 +31,7 @@
       Toplevel.keep (print_provers o Toplevel.theory_of)));
 
 val _ =
-  OuterSyntax.command "sledgehammer"
+  OuterSyntax.improper_command "sledgehammer"
     "search for first-order proof using automatic theorem provers" K.diag
     (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
       Toplevel.keep (sledgehammer names o Toplevel.proof_of)));
@@ -77,7 +77,7 @@
 val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel)
 
 val _ =
-  OuterSyntax.command "atp_minimize" "minimize theorem list with external prover" K.diag
+  OuterSyntax.improper_command "atp_minimize" "minimize theorem list with external prover" K.diag
     (parse_args -- parse_thm_names >> (fn (args, thm_names) =>
       Toplevel.no_timing o Toplevel.unknown_proof o
         Toplevel.keep (atp_minimize_command args thm_names o Toplevel.proof_of)))