--- a/src/Pure/meta_simplifier.ML Tue Oct 20 20:03:23 2009 +0200
+++ b/src/Pure/meta_simplifier.ML Tue Oct 20 20:54:31 2009 +0200
@@ -1158,8 +1158,8 @@
let
val prem' = Thm.rhs_of eqn;
val tprems = map term_of prems;
- val i = 1 + Library.foldl Int.max (~1, map (fn p =>
- find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn)));
+ val i = 1 + fold Integer.max (map (fn p =>
+ find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn))) ~1;
val (rrs', asm') = rules_of_prem ss prem'
in mut_impc prems concl rrss asms (prem' :: prems')
(rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true)