1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jul 23 15:32:30 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jul 23 15:32:30 2012 +0200
     1.3 @@ -774,7 +774,7 @@
     1.4                val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
     1.5              in (reps, (n, next_commit, timed_out)) end
     1.6          val n =
     1.7 -          if null old_facts then
     1.8 +          if not atp orelse null old_facts then
     1.9              n
    1.10            else
    1.11              let