--- a/src/Pure/meta_simplifier.ML Tue Oct 27 22:55:27 2009 +0100
+++ b/src/Pure/meta_simplifier.ML Tue Oct 27 22:56:14 2009 +0100
@@ -1139,8 +1139,8 @@
end
and mut_impc [] concl [] [] prems' rrss' asms' eqns ss changed k =
- transitive1 (Library.foldl (fn (eq2, (eq1, prem)) => transitive1 eq1
- (Option.map (disch false prem) eq2)) (NONE, eqns ~~ prems'))
+ transitive1 (fold (fn (eq1, prem) => fn eq2 => transitive1 eq1
+ (Option.map (disch false prem) eq2)) (eqns ~~ prems') NONE)
(if changed > 0 then
mut_impc (rev prems') concl (rev rrss') (rev asms')
[] [] [] [] ss ~1 changed