Replaced min by Int.min
authorpaulson
Fri Nov 01 15:15:39 1996 +0100 (1996-11-01)
changeset 2143093bbe6d333b
parent 2142 20f208ff085d
child 2144 ddb8499c772b
Replaced min by Int.min
src/Provers/hypsubst.ML
src/Provers/splitter.ML
src/Pure/search.ML
     1.1 --- a/src/Provers/hypsubst.ML	Fri Nov 01 15:14:25 1996 +0100
     1.2 +++ b/src/Provers/hypsubst.ML	Fri Nov 01 15:15:39 1996 +0100
     1.3 @@ -120,7 +120,7 @@
     1.4  			      1 + count Bs)
     1.5                               handle Match => 0)
     1.6  	val (_,_,Bi,_) = dest_state(state,i)
     1.7 -        val j = min [m, count (Logic.strip_assums_hyp Bi)]
     1.8 +        val j = Int.min(m, count (Logic.strip_assums_hyp Bi))
     1.9      in  REPEAT_DETERM_N j     (etac thin_rl i)   THEN
    1.10          REPEAT_DETERM_N (m-j) (etac revcut_rl i)
    1.11      end);
     2.1 --- a/src/Provers/splitter.ML	Fri Nov 01 15:14:25 1996 +0100
     2.2 +++ b/src/Provers/splitter.ML	Fri Nov 01 15:15:39 1996 +0100
     2.3 @@ -102,7 +102,7 @@
     2.4     has a body of type T; otherwise the expansion thm will fail later on
     2.5  *)
     2.6  fun type_test(T,lbnos,apsns) =
     2.7 -  let val (_,U,_) = nth_elem(min lbnos,apsns)
     2.8 +  let val (_,U,_) = nth_elem(foldl Int.min (hd lbnos, tl lbnos), apsns)
     2.9    in T=U end;
    2.10  
    2.11  (*************************************************************************
    2.12 @@ -139,7 +139,8 @@
    2.13             val flbnos = filter (fn i => i < lev) lbnos
    2.14             val tt = incr_bv(~lev,0,t)
    2.15         in if null flbnos then [(thm,[],pos,TB,tt)]
    2.16 -          else if type_test(T,flbnos,apsns) then [(thm, rev apsns,pos,TB,tt)] else []
    2.17 +          else if type_test(T,flbnos,apsns) then [(thm, rev apsns,pos,TB,tt)] 
    2.18 +               else []
    2.19         end;
    2.20  
    2.21  
     3.1 --- a/src/Pure/search.ML	Fri Nov 01 15:14:25 1996 +0100
     3.2 +++ b/src/Pure/search.ML	Fri Nov 01 15:15:39 1996 +0100
     3.3 @@ -136,7 +136,7 @@
     3.4                     val rgd' = not (has_vars (hd (prems_of st)))
     3.5                     val k' = k+np'-np+1  (*difference in # of subgoals, +1*)
     3.6                 in  if k'+np' >= bnd 
     3.7 -		   then depth (bnd, min [inc, k'+np'+1-bnd]) qs
     3.8 +		   then depth (bnd, Int.min(inc, k'+np'+1-bnd)) qs
     3.9  		   else if np' < np (*solved a subgoal; prune rigid ancestors*)
    3.10                     then depth (bnd,inc) 
    3.11  		         (prune ((k', np', rgd', tf st), (k,np,rgd,stq) :: qs))