--- 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)