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