src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
changeset 57783 2bf99b3f62e1
parent 57750 670cbec816b9
child 58061 3d060f43accb
--- 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,