--- a/src/Pure/drule.ML Sat Oct 07 01:31:08 2006 +0200
+++ b/src/Pure/drule.ML Sat Oct 07 01:31:09 2006 +0200
@@ -128,6 +128,7 @@
val termI: thm
val mk_term: cterm -> thm
val dest_term: thm -> cterm
+ val term_rule: theory -> (thm -> thm) -> term -> term
val sort_triv: theory -> typ * sort -> thm list
val unconstrainTs: thm -> thm
val rename_bvars: (string * string) list -> thm -> thm
@@ -981,6 +982,9 @@
else raise THM ("dest_term", 0, [th])
end;
+fun term_rule thy f t =
+ Thm.term_of (dest_term (f (mk_term (Thm.cterm_of thy t))));
+
(** variations on instantiate **)