src/Pure/Proof/proof_rewrite_rules.ML
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;