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