Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Changed interface of rewrite_term.
authorberghofe
Fri, 31 May 2002 18:48:31 +0200
changeset 13196 08c42252346f
parent 13195 98975cc13d28
child 13197 0567f4fd1415
Changed interface of rewrite_term.
src/Pure/meta_simplifier.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle