src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

                 else
                   (reps, next_commit)
               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
               fun priority_of (_, th) =
                 random_range 0 (1000 * max_dependencies)