1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Jul 23 15:32:30 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Jul 23 15:32:30 2012 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4  open Sledgehammer_MaSh
     1.5  open Sledgehammer_Run
     1.6  
     1.7 -val cvc3N = "cvc3"
     1.8 +(* val cvc3N = "cvc3" *)
     1.9  val yicesN = "yices"
    1.10  val z3N = "z3"
    1.11  

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jul 23 15:32:30 2012 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jul 23 15:32:30 2012 +0200
     2.3 @@ -774,7 +774,7 @@
     2.4                val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
     2.5              in (reps, (n, next_commit, timed_out)) end
     2.6          val n =
     2.7 -          if null old_facts then
     2.8 +          if not atp orelse null old_facts then
     2.9              n
    2.10            else
    2.11              let