1.1 --- a/src/Pure/meta_simplifier.ML	Fri May 31 18:47:11 2002 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Fri May 31 18:48:31 2002 +0200
     1.3 @@ -54,7 +54,7 @@
     1.4    val rewrite_goal_rule : bool* bool * bool
     1.5                            -> (meta_simpset -> thm -> thm option)
     1.6                            -> meta_simpset -> int -> thm -> thm
     1.7 -  val rewrite_term: Sign.sg -> thm list -> term -> term
     1.8 +  val rewrite_term: Sign.sg -> thm list -> (term -> term option) list -> term -> term
     1.9  end;
    1.10  
    1.11  structure MetaSimplifier : META_SIMPLIFIER =
    1.12 @@ -987,7 +987,8 @@
    1.13  
    1.14  
    1.15  (*simple term rewriting -- without proofs*)
    1.16 -fun rewrite_term sg rules = Pattern.rewrite_term (Sign.tsig_of sg) (map decomp_simp' rules);
    1.17 +fun rewrite_term sg rules procs =
    1.18 +  Pattern.rewrite_term (Sign.tsig_of sg) (map decomp_simp' rules) procs;
    1.19  
    1.20  end;
    1.21