# HG changeset patch
# User blanchet
# Date 1369119778 -7200
# Node ID f5280907284d1a53fd523897fc6cfca45d1b3b22
# Parent  895d12fc0dd7cd508ae7d1e2d130562472a49ccc
added compatibility alias

diff -r 895d12fc0dd7 -r f5280907284d src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon May 20 20:54:11 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue May 21 09:02:58 2013 +0200
@@ -108,7 +108,8 @@
 val alias_params =
   [("prover", ("provers", [])), (* undocumented *)
    ("dont_preplay", ("preplay_timeout", ["0"])),
-   ("dont_compress_isar", ("isar_compress", ["0"]))]
+   ("dont_compress_isar", ("isar_compress", ["0"])),
+   ("isar_proof", ("isar_proofs", [])) (* legacy *)]
 val negated_alias_params =
   [("no_debug", "debug"),
    ("quiet", "verbose"),