# HG changeset patch
# User wenzelm
# Date 1160177469 -7200
# Node ID 54481abec257448582287a24a9a682efe6961ead
# Parent  b853d43268945133d6e688cf4b1d07ca2112d8d1
added term_rule;

diff -r b853d4326894 -r 54481abec257 src/Pure/drule.ML
--- 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 **)