diff -r fa8e32209734 -r 1e9e0f5877f2 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Wed Aug 03 16:24:52 2005 +0200
+++ b/src/Pure/proof_general.ML	Wed Aug 03 16:25:22 2005 +0200
@@ -495,8 +495,8 @@
   let
     val names = filter_out (equal "") (map Thm.name_of_thm ths);
     val deps = filter_out (equal "")
-      (Symtab.keys (Library.foldl (uncurry Proofterm.thms_of_proof)
-        (Symtab.empty, map Thm.proof_of ths)));
+      (Symtab.keys (fold Proofterm.thms_of_proof
+        (map Thm.proof_of ths) Symtab.empty));
   in
     if null names orelse null deps then ()
     else thm_deps_message (spaces_quote names, spaces_quote deps)