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))