src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

    ("preplay_timeout", "3")]
 
 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"),
    ("no_overlord", "overlord"),
    ("non_blocking", "blocking"),