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