src/Provers/hypsubst.ML
changeset 2143 093bbe6d333b
parent 1011 5c9654e2e3de
child 2174 0829b7b632c5
     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);