--- a/src/HOL/Tools/SMT/smt_translate.ML Thu Nov 25 14:36:51 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML Thu Nov 25 14:59:01 2010 +0100
@@ -402,6 +402,9 @@
| NONE => transs h T ts))
| (h as Free (_, T), ts) => transs h T ts
| (Bound i, []) => pair (SVar i)
+ | (Abs (_, _, t1 $ Bound 0), []) =>
+ if not (loose_bvar1 (t1, 0)) then trans t1 (* eta-reduce on the fly *)
+ else raise TERM ("smt_translate", [t])
| _ => raise TERM ("smt_translate", [t]))
and transs t T ts =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Nov 25 14:36:51 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Nov 25 14:59:01 2010 +0100
@@ -104,8 +104,9 @@
else is_atp_installed thy name
end
-val smt_default_max_relevant = 200 (* FUDGE *)
-val auto_max_relevant_divisor = 2 (* FUDGE *)
+(* FUDGE *)
+val smt_default_max_relevant = 200
+val auto_max_relevant_divisor = 2
fun default_max_relevant_for_prover thy name =
if is_smt_prover name then smt_default_max_relevant
@@ -432,6 +433,7 @@
| failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
| failure_from_smt_failure _ = UnknownError
+(* FUDGE *)
val smt_max_iter = 8
val smt_iter_fact_divisor = 2
val smt_iter_min_msecs = 5000