--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Aug 04 14:19:43 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Aug 04 15:02:02 2014 +0200
@@ -35,7 +35,7 @@
max_mono_iters : int option,
max_new_mono_instances : int option,
isar_proofs : bool option,
- compress : real,
+ compress : real option,
try0 : bool,
smt_proofs : bool option,
slice : bool,
@@ -126,7 +126,7 @@
max_mono_iters : int option,
max_new_mono_instances : int option,
isar_proofs : bool option,
- compress : real,
+ compress : real option,
try0 : bool,
smt_proofs : bool option,
slice : bool,