--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Sep 20 22:39:30 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Sep 20 22:39:30 2013 +0200
@@ -94,7 +94,6 @@
("max_new_mono_instances", "smart"),
("isar_proofs", "smart"),
("isar_compress", "10"),
- ("isar_compress_degree", "2"), (* TODO: document *)
("isar_try0", "true"), (* TODO: document *)
("isar_minimize", "true"), (* TODO: document *)
("slice", "true"),
@@ -304,7 +303,6 @@
lookup_option lookup_int "max_new_mono_instances"
val isar_proofs = lookup_option lookup_bool "isar_proofs"
val isar_compress = Real.max (1.0, lookup_real "isar_compress")
- val isar_compress_degree = Int.max (1, lookup_int "isar_compress_degree")
val isar_try0 = lookup_bool "isar_try0"
val isar_minimize = lookup_bool "isar_minimize"
val slice = mode <> Auto_Try andalso lookup_bool "slice"
@@ -322,10 +320,9 @@
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,
- isar_compress = isar_compress, isar_compress_degree = isar_compress_degree,
- isar_try0 = isar_try0, isar_minimize = isar_minimize, slice = slice,
- minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
- expect = expect}
+ isar_compress = isar_compress, isar_try0 = isar_try0,
+ isar_minimize = isar_minimize, slice = slice, minimize = minimize,
+ timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
end
fun get_params mode = extract_params mode o default_raw_params