--- 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' [])