diff -r 98975cc13d28 -r 08c42252346f src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Fri May 31 18:47:11 2002 +0200
+++ b/src/Pure/meta_simplifier.ML	Fri May 31 18:48:31 2002 +0200
@@ -54,7 +54,7 @@
   val rewrite_goal_rule : bool* bool * bool
                           -> (meta_simpset -> thm -> thm option)
                           -> meta_simpset -> int -> thm -> thm
-  val rewrite_term: Sign.sg -> thm list -> term -> term
+  val rewrite_term: Sign.sg -> thm list -> (term -> term option) list -> term -> term
 end;
 
 structure MetaSimplifier : META_SIMPLIFIER =
@@ -987,7 +987,8 @@
 
 
 (*simple term rewriting -- without proofs*)
-fun rewrite_term sg rules = Pattern.rewrite_term (Sign.tsig_of sg) (map decomp_simp' rules);
+fun rewrite_term sg rules procs =
+  Pattern.rewrite_term (Sign.tsig_of sg) (map decomp_simp' rules) procs;
 
 end;