Adapted to new interface of thms_of_proof.

--- a/src/Pure/Proof/proof_rewrite_rules.ML	Wed Aug 03 16:24:52 2005 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Wed Aug 03 16:25:22 2005 +0200
@@ -247,7 +247,7 @@
             if s mem defnames then []
             else map (pair s o SOME o fst) (filter_out (fn (p, _) =>
               null (term_consts p inter cnames)) ps))
-          (Symtab.dest (thms_of_proof Symtab.empty prf)))
+          (Symtab.dest (thms_of_proof prf Symtab.empty)))
       in Reconstruct.expand_proof sign thms end
   in
     rewrite_terms (Pattern.rewrite_term tsig defs' [])

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