# HG changeset patch
# User blanchet
# Date 1307700075 -7200
# Node ID 6c008d3efb0a3d5b3a28c2ed52271b8f49ab2150
# Parent  597f31069e1802ab62f5af4eefddcfd563267cec
removed "atp" and "atps" aliases, which users should have forgotten by now if they ever used them

diff -r 597f31069e18 -r 6c008d3efb0a src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jun 10 12:01:15 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jun 10 12:01:15 2011 +0200
@@ -102,9 +102,7 @@
    ("preplay_timeout", "4")]
 
 val alias_params =
-  [("prover", "provers"),
-   ("atps", "provers"), (* FIXME: legacy *)
-   ("atp", "provers")]  (* FIXME: legacy *)
+  [("prover", "provers")]
 val negated_alias_params =
   [("no_debug", "debug"),
    ("quiet", "verbose"),