diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Thu Apr 27 12:11:56 2006 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Thu Apr 27 15:06:35 2006 +0200
@@ -246,11 +246,11 @@
     val f = if not r then I else
       let
         val cnames = map (fst o dest_Const o fst) defs';
-        val thms = List.concat (map (fn (s, ps) =>
+        val thms = maps (fn (s, ps) =>
             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 prf Symtab.empty)))
+          (Symtab.dest (thms_of_proof prf Symtab.empty))
       in Reconstruct.expand_proof thy thms end
   in
     rewrite_terms (Pattern.rewrite_term thy defs' [])