--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Jun 12 17:02:03 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Jun 12 17:10:12 2014 +0200
@@ -94,8 +94,8 @@
("max_mono_iters", "smart"),
("max_new_mono_instances", "smart"),
("isar_proofs", "smart"),
- ("compress_isar", "10"),
- ("try0_isar", "true"),
+ ("compress", "10"),
+ ("try0", "true"),
("smt_proofs", "smart"),
("slice", "true"),
("minimize", "smart"),
@@ -104,7 +104,7 @@
val alias_params =
[("prover", ("provers", [])), (* undocumented *)
("dont_preplay", ("preplay_timeout", ["0"])),
- ("dont_compress_isar", ("compress_isar", ["0"])),
+ ("dont_compress", ("compress", ["0"])),
("isar_proof", ("isar_proofs", [])) (* legacy *)]
val negated_alias_params =
[("no_debug", "debug"),
@@ -118,7 +118,7 @@
("no_isar_proofs", "isar_proofs"),
("dont_slice", "slice"),
("dont_minimize", "minimize"),
- ("dont_try0_isar", "try0_isar"),
+ ("dont_try0", "try0"),
("no_smt_proofs", "smt_proofs")]
val params_not_for_minimize =
@@ -299,8 +299,8 @@
val max_new_mono_instances =
lookup_option lookup_int "max_new_mono_instances"
val isar_proofs = lookup_option lookup_bool "isar_proofs"
- val compress_isar = Real.max (1.0, lookup_real "compress_isar")
- val try0_isar = lookup_bool "try0_isar"
+ val compress = Real.max (1.0, lookup_real "compress")
+ val try0 = lookup_bool "try0"
val smt_proofs = lookup_option lookup_bool "smt_proofs"
val slice = mode <> Auto_Try andalso lookup_bool "slice"
val minimize = if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
@@ -313,8 +313,8 @@
uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
- compress_isar = compress_isar, try0_isar = try0_isar, smt_proofs = smt_proofs, slice = slice,
- minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
+ compress = compress, try0 = try0, smt_proofs = smt_proofs, slice = slice, minimize = minimize,
+ timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
end
fun get_params mode = extract_params mode o default_raw_params mode