# HG changeset patch
# User blanchet
# Date 1360916246 -3600
# Node ID 583a37b9512da88a1f3b11d58c7f7c366b2ca997
# Parent  077456580eca08304e85378d9730ae3771075b45
killed legacy alias

diff -r 077456580eca -r 583a37b9512d src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Feb 15 09:17:20 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Feb 15 09:17:26 2013 +0100
@@ -101,8 +101,7 @@
    ("preplay_timeout", "3")]
 
 val alias_params =
-  [("prover", ("provers", [])), (* legacy *)
-   ("max_relevant", ("max_facts", [])), (* legacy *)
+  [("prover", ("provers", [])), (* undocumented *)
    ("dont_preplay", ("preplay_timeout", ["0"]))]
 val negated_alias_params =
   [("no_debug", "debug"),