src/Pure/search.ML

   The solution sequence is redundant: the cutoff heuristic makes it impossible
   to suppress solutions arising from earlier searches, as the accumulated cost
   (k) can be wrong.*)
 fun THEN_ITER_DEEPEN lim tac0 satp tac1 st =
   let
-    val countr = Unsynchronized.ref 0
+    val counter = Unsynchronized.ref 0
     and tf = tac1 1
     and qs0 = tac0 st
      (*bnd = depth bound; inc = estimate of increment required next*)
     fun depth (bnd, inc) [] =
           if bnd > lim then NONE

             (*larger increments make it run slower for the hard problems*)
             depth (bnd + inc, 10) [(0, 1, false, qs0)]
       | depth (bnd, inc) ((k, np, rgd, q) :: qs) =
           if k >= bnd then depth (bnd, inc) qs
           else
-           (case (Unsynchronized.inc countr; Seq.pull q) of
+           (case (Unsynchronized.inc counter; Seq.pull q) of
              NONE => depth (bnd, inc) qs
            | SOME (st, stq) =>
               if satp st then (*solution!*)
                 SOME(st, Seq.make (fn() => depth (bnd, inc) ((k, np, rgd, stq) :: qs)))
               else