# HG changeset patch
# User wenzelm
# Date 1460194463 -7200
# Node ID 9eb0359d6a77f9600ee3fadce701e838c27f74de
# Parent  2fcbd4abc021f76d447584e2a79848048975e853
tuned;

diff -r 2fcbd4abc021 -r 9eb0359d6a77 src/Pure/search.ML
--- a/src/Pure/search.ML	Sat Apr 09 11:21:38 2016 +0200
+++ b/src/Pure/search.ML	Sat Apr 09 11:34:23 2016 +0200
@@ -108,7 +108,7 @@
   (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*)
@@ -120,7 +120,7 @@
       | 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!*)