fixed typo in option name
authorblanchet
Wed, 20 Feb 2013 09:58:28 +0100
changeset 51195 d995fae02981
parent 51194 53a496954928
child 51196 1ff19dfd3111
fixed typo in option name
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"),