discontinued Drule.term_rule, which tends to cause confusion due to builtin cterm_of (NB: the standard morphisms already provide a separate term component);

--- a/src/HOL/Tools/Function/function_common.ML	Wed Feb 15 21:38:28 2012 +0100
+++ b/src/HOL/Tools/Function/function_common.ML	Wed Feb 15 22:44:31 2012 +0100
@@ -120,10 +120,9 @@
 
 val get_function = FunctionData.get o Context.Proof;
 
-
 fun lift_morphism thy f =
   let
-    val term = Drule.term_rule thy f
+    fun term t = Thm.term_of (Drule.cterm_rule f (Thm.cterm_of thy t))
   in
     Morphism.thm_morphism f $> Morphism.term_morphism term
     $> Morphism.typ_morphism (Logic.type_map term)

--- a/src/Pure/drule.ML	Wed Feb 15 21:38:28 2012 +0100
+++ b/src/Pure/drule.ML	Wed Feb 15 22:44:31 2012 +0100
@@ -95,7 +95,6 @@
   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 dummy_thm: thm
   val sort_constraintI: thm
   val sort_constraint_eq: thm
@@ -720,7 +719,6 @@
   end;
 
 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));
 
 val dummy_thm = mk_term (certify Term.dummy_prop);