killed legacy alias
authorblanchet
Fri, 15 Feb 2013 09:17:26 +0100
changeset 51138 583a37b9512d
parent 51137 077456580eca
child 51140 59e311235de4
child 51145 280ece22765b
killed legacy alias
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"),