# HG changeset patch
# User paulson
# Date 846857739 -3600
# Node ID 093bbe6d333bfef0012ad6e9469f9888f9eefe71
# Parent  20f208ff085dbdb238bd1435719a3d860c958f4c
Replaced min by Int.min

diff -r 20f208ff085d -r 093bbe6d333b src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Fri Nov 01 15:14:25 1996 +0100
+++ b/src/Provers/hypsubst.ML	Fri Nov 01 15:15:39 1996 +0100
@@ -120,7 +120,7 @@
 			      1 + count Bs)
                              handle Match => 0)
 	val (_,_,Bi,_) = dest_state(state,i)
-        val j = min [m, count (Logic.strip_assums_hyp Bi)]
+        val j = Int.min(m, count (Logic.strip_assums_hyp Bi))
     in  REPEAT_DETERM_N j     (etac thin_rl i)   THEN
         REPEAT_DETERM_N (m-j) (etac revcut_rl i)
     end);
diff -r 20f208ff085d -r 093bbe6d333b src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Fri Nov 01 15:14:25 1996 +0100
+++ b/src/Provers/splitter.ML	Fri Nov 01 15:15:39 1996 +0100
@@ -102,7 +102,7 @@
    has a body of type T; otherwise the expansion thm will fail later on
 *)
 fun type_test(T,lbnos,apsns) =
-  let val (_,U,_) = nth_elem(min lbnos,apsns)
+  let val (_,U,_) = nth_elem(foldl Int.min (hd lbnos, tl lbnos), apsns)
   in T=U end;
 
 (*************************************************************************
@@ -139,7 +139,8 @@
            val flbnos = filter (fn i => i < lev) lbnos
            val tt = incr_bv(~lev,0,t)
        in if null flbnos then [(thm,[],pos,TB,tt)]
-          else if type_test(T,flbnos,apsns) then [(thm, rev apsns,pos,TB,tt)] else []
+          else if type_test(T,flbnos,apsns) then [(thm, rev apsns,pos,TB,tt)] 
+               else []
        end;
 
 
diff -r 20f208ff085d -r 093bbe6d333b src/Pure/search.ML
--- 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))