# HG changeset patch
# User wenzelm
# Date 869646168 -7200
# Node ID 5a720f6b9f38c803d42d3c7038be0f0d6584e595
# Parent  b1013660aeff39d3c9355639d426e13c4ed5fe7e
added rewrite_thm;

diff -r b1013660aeff -r 5a720f6b9f38 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Wed Jul 23 10:22:30 1997 +0200
+++ b/src/Pure/drule.ML	Wed Jul 23 10:22:48 1997 +0200
@@ -46,10 +46,12 @@
   val reflexive_thm	: thm
   val refl_implies      : thm
   val revcut_rl		: thm
-  val rewrite_goal_rule	: bool*bool -> (meta_simpset -> thm -> thm option)
+  val rewrite_goal_rule	: bool * bool -> (meta_simpset -> thm -> thm option)
         -> meta_simpset -> int -> thm -> thm
   val rewrite_goals_rule: thm list -> thm -> thm
   val rewrite_rule	: thm list -> thm -> thm
+  val rewrite_thm	: bool * bool -> (meta_simpset -> thm -> thm option)
+	-> meta_simpset -> thm -> thm
   val RS		: thm * thm -> thm
   val RSN		: thm * (int * thm) -> thm
   val RL		: thm list * thm list -> thm list
@@ -509,7 +511,6 @@
 
 (*** Meta-Rewriting Rules ***)
 
-
 val reflexive_thm =
   let val cx = cterm_of Sign.proto_pure (Var(("x",0),TVar(("'a",0),logicS)))
   in Thm.reflexive cx end;
@@ -551,6 +552,8 @@
   | rewrite_rule thms th =
 	fconv_rule (rew_conv (true,false) (K(K None)) (Thm.mss_of thms)) th;
 
+fun rewrite_thm mode prover mss = fconv_rule (rew_conv mode prover mss);
+
 (*Rewrite the subgoals of a proof state (represented by a theorem) *)
 fun rewrite_goals_rule []   th = th
   | rewrite_goals_rule thms th =