# HG changeset patch
# User blanchet
# Date 1361350708 -3600
# Node ID d995fae02981067027faa0488970953687a1e4e0
# Parent  53a4969549289eaefb28981191462bb2fef2abc2
fixed typo in option name

diff -r 53a496954928 -r d995fae02981 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Feb 20 08:56:34 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Feb 20 09:58:28 2013 +0100
@@ -103,7 +103,7 @@
 val alias_params =
   [("prover", ("provers", [])), (* undocumented *)
    ("dont_preplay", ("preplay_timeout", ["0"])),
-   ("dont_compress_isar", ("compress_isar", ["0"]))]
+   ("dont_compress_isar", ("isar_compress", ["0"]))]
 val negated_alias_params =
   [("no_debug", "debug"),
    ("quiet", "verbose"),