Mercurialisabelle / diff
summary | shortlog | changelog | graph | tags | branches | files | changeset | file | revisions | annotate | diff | raw
src/Pure/search.ML
changeset 2143 093bbe6d333b
parent 1588 fff3738830f5
child 2672 85d7e800d754 
     1.1 --- a/src/Pure/search.ML	Fri Nov 01 15:14:25 1996 +0100
     1.2 +++ b/src/Pure/search.ML	Fri Nov 01 15:15:39 1996 +0100
     1.3 @@ -136,7 +136,7 @@
     1.4                     val rgd' = not (has_vars (hd (prems_of st)))
     1.5                     val k' = k+np'-np+1  (*difference in # of subgoals, +1*)
     1.6                 in  if k'+np' >= bnd 
     1.7 -		   then depth (bnd, min [inc, k'+np'+1-bnd]) qs
     1.8 +		   then depth (bnd, Int.min(inc, k'+np'+1-bnd)) qs
     1.9  		   else if np' < np (*solved a subgoal; prune rigid ancestors*)
    1.10                     then depth (bnd,inc) 
    1.11  		         (prune ((k', np', rgd', tf st), (k,np,rgd,stq) :: qs))
isabelle