src/Pure/search.ML
changeset 2143 093bbe6d333b
parent 1588 fff3738830f5
child 2672 85d7e800d754
--- a/src/Pure/search.ML	Fri Nov 01 15:14:25 1996 +0100
+++ b/src/Pure/search.ML	Fri Nov 01 15:15:39 1996 +0100
@@ -136,7 +136,7 @@
                    val rgd' = not (has_vars (hd (prems_of st)))
                    val k' = k+np'-np+1  (*difference in # of subgoals, +1*)
                in  if k'+np' >= bnd 
-		   then depth (bnd, min [inc, k'+np'+1-bnd]) qs
+		   then depth (bnd, Int.min(inc, k'+np'+1-bnd)) qs
 		   else if np' < np (*solved a subgoal; prune rigid ancestors*)
                    then depth (bnd,inc) 
 		         (prune ((k', np', rgd', tf st), (k,np,rgd,stq) :: qs))