src/Pure/Proof/proof_rewrite_rules.ML

       let
         val cnames = map (fst o dest_Const o fst) defs';
         val thms = flat (map (fn (s, ps) =>
             if s mem defnames then []
             else map (pair s o Some o fst) (filter_out (fn (p, _) =>
-              null (add_term_consts (p, []) inter cnames)) ps))
+              null (term_consts p inter cnames)) ps))
           (Symtab.dest (thms_of_proof Symtab.empty prf)))
       in Reconstruct.expand_proof sign thms end
   in
     rewrite_terms (Pattern.rewrite_term tsig defs' [])
       (insert_refl defnames [] (f prf))