| changeset 13198 | 3e40f48a500f |
| parent 12906 | 165f4e1937f4 |
| child 13257 | 1b7104a1c0bd |
--- a/src/Pure/Proof/proof_rewrite_rules.ML Fri May 31 18:49:31 2002 +0200 +++ b/src/Pure/Proof/proof_rewrite_rules.ML Fri May 31 18:50:03 2002 +0200 @@ -247,7 +247,7 @@ null (foldr add_term_consts (map fst ps, []) inter cnames)) (Symtab.dest (thms_of_proof Symtab.empty prf))) \\ defnames in - rewrite_terms (Pattern.rewrite_term tsig defs') (insert_refl defnames [] + rewrite_terms (Pattern.rewrite_term tsig defs' []) (insert_refl defnames [] (Reconstruct.expand_proof sign thmnames prf)) end;