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