# HG changeset patch
# User wenzelm
# Date 1011219464 -3600
# Node ID 36ca5ea8092c7b3a715ded8d94d0086062e95ee2
# Parent  a4183c50ae5f8df983ef60cf43687fc532301f81
interface to Pattern.rewrite_term;

diff -r a4183c50ae5f -r 36ca5ea8092c src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Wed Jan 16 22:24:37 2002 +0100
+++ b/src/Pure/meta_simplifier.ML	Wed Jan 16 23:17:44 2002 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/meta_simplifier.ML
     ID:         $Id$
     Author:     Tobias Nipkow and Stefan Berghofer
-    Copyright   1994  University of Cambridge
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Meta-level Simplification.
 *)
@@ -54,6 +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
 end;
 
 structure MetaSimplifier : META_SIMPLIFIER =
@@ -284,6 +285,12 @@
                  andalso not (is_Var (term_of elhs))
   in (sign, prems, term_of lhs, elhs, term_of rhs, perm) end;
 
+fun decomp_simp' thm =
+  let val (_, _, _, elhs, rhs, _) = decomp_simp thm in
+    if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", thm)
+    else (term_of elhs, rhs)
+  end;
+
 fun mk_eq_True (Mss{mk_rews={mk_eq_True,...},...}) thm =
   case mk_eq_True thm of
     None => []
@@ -978,6 +985,10 @@
   then fconv_rule (goals_conv (fn j => j=i) (rewrite_cterm mode prover mss)) thm
   else raise THM("rewrite_goal_rule",i,[thm]);
 
+
+(*simple term rewriting -- without proofs*)
+fun rewrite_term sg rules = Pattern.rewrite_term (Sign.tsig_of sg) (map decomp_simp' rules);
+
 end;
 
 structure BasicMetaSimplifier: BASIC_META_SIMPLIFIER = MetaSimplifier;