# HG changeset patch
# User wenzelm
# Date 898780859 -7200
# Node ID 2a8ed71f791ff629cd751f3f18eeeaed12a2a03f
# Parent  7b5ea59c0275e63bfe2a83cafa6d354109842df8
added rewrite_cterm;

diff -r 7b5ea59c0275 -r 2a8ed71f791f src/Pure/drule.ML
--- a/src/Pure/drule.ML	Thu Jun 25 13:57:34 1998 +0200
+++ b/src/Pure/drule.ML	Thu Jun 25 15:20:59 1998 +0200
@@ -56,6 +56,9 @@
   val rewrite_thm	: bool * bool * bool
                           -> (meta_simpset -> thm -> thm option)
                           -> meta_simpset -> thm -> thm
+  val rewrite_cterm	: bool * bool * bool
+                          -> (meta_simpset -> thm -> thm option)
+                          -> meta_simpset -> cterm -> thm
   val rewrite_goals_rule_aux: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
   val rewrite_goal_rule	: bool* bool * bool
                           -> (meta_simpset -> thm -> thm option)
@@ -452,6 +455,7 @@
       fconv_rule (rew_conv (true,false,false) prover (Thm.mss_of thms)) th;
 
 fun rewrite_thm mode prover mss = fconv_rule (rew_conv mode prover mss);
+fun rewrite_cterm mode prover mss = Thm.rewrite_cterm mode mss prover;
 
 (*Rewrite the subgoals of a proof state (represented by a theorem) *)
 fun rewrite_goals_rule_aux _ []   th = th