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