equal
deleted
inserted
replaced
772 else |
772 else |
773 (reps, next_commit) |
773 (reps, next_commit) |
774 val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout) |
774 val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout) |
775 in (reps, (n, next_commit, timed_out)) end |
775 in (reps, (n, next_commit, timed_out)) end |
776 val n = |
776 val n = |
777 if null old_facts then |
777 if not atp orelse null old_facts then |
778 n |
778 n |
779 else |
779 else |
780 let |
780 let |
781 fun priority_of (_, th) = |
781 fun priority_of (_, th) = |
782 random_range 0 (1000 * max_dependencies) |
782 random_range 0 (1000 * max_dependencies) |