# HG changeset patch
# User wenzelm
# Date 1164402315 -3600
# Node ID 33f109ea389f630f2aeccb088c60c76eb93710f6
# Parent  571b8cd087f817f08970515baccd35a864b5978e
added cterm_rule;

diff -r 571b8cd087f8 -r 33f109ea389f src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Nov 24 22:05:14 2006 +0100
+++ b/src/Pure/drule.ML	Fri Nov 24 22:05:15 2006 +0100
@@ -128,6 +128,7 @@
   val termI: thm
   val mk_term: cterm -> thm
   val dest_term: thm -> cterm
+  val cterm_rule: (thm -> thm) -> cterm -> cterm
   val term_rule: theory -> (thm -> thm) -> term -> term
   val sort_triv: theory -> typ * sort -> thm list
   val unconstrainTs: thm -> thm
@@ -968,8 +969,8 @@
     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))));
+fun cterm_rule f = dest_term o f o mk_term;
+fun term_rule thy f t = Thm.term_of (cterm_rule f (Thm.cterm_of thy t));