# HG changeset patch
# User berghofe
# Date 1022863803 -7200
# Node ID 3e40f48a500fe59c5c988f09c8f547ae384d3f4f
# Parent  0567f4fd1415fcfbe33ea85c9fc61fd3ae3340ab
Changed interface of Pattern.rewrite_term.

diff -r 0567f4fd1415 -r 3e40f48a500f src/Pure/Proof/proof_rewrite_rules.ML
--- 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;
 
diff -r 0567f4fd1415 -r 3e40f48a500f src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri May 31 18:49:31 2002 +0200
+++ b/src/Pure/drule.ML	Fri May 31 18:50:03 2002 +0200
@@ -705,7 +705,7 @@
 
 fun norm_hhf sg t =
   if is_norm_hhf t then t
-  else Pattern.rewrite_term (Sign.tsig_of sg) [Logic.dest_equals (prop_of norm_hhf_eq)] t;
+  else Pattern.rewrite_term (Sign.tsig_of sg) [Logic.dest_equals (prop_of norm_hhf_eq)] [] t;
 
 
 (*** Instantiate theorem th, reading instantiations under signature sg ****)