Changed interface of Pattern.rewrite_term.

--- 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;
 

--- 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 ****)