src/Pure/drule.ML
changeset 5079 2a8ed71f791f
parent 4789 9cf0073bbe2b
child 5311 f3f71669878e
--- 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