changeset 2143 | 093bbe6d333b |
parent 1011 | 5c9654e2e3de |
child 2174 | 0829b7b632c5 |
--- 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);