--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jul 23 15:32:30 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jul 23 15:32:30 2012 +0200
@@ -29,7 +29,7 @@
open Sledgehammer_MaSh
open Sledgehammer_Run
-val cvc3N = "cvc3"
+(* val cvc3N = "cvc3" *)
val yicesN = "yices"
val z3N = "z3"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Jul 23 15:32:30 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Jul 23 15:32:30 2012 +0200
@@ -774,7 +774,7 @@
val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
in (reps, (n, next_commit, timed_out)) end
val n =
- if null old_facts then
+ if not atp orelse null old_facts then
n
else
let