# HG changeset patch
# User wenzelm
# Date 1329342271 -3600
# Node ID b8920f3fd259b2e851a55899a37ca2cd1be064ad
# Parent  8e8a339e176f84cc24f18333862096b038c0dc38
discontinued Drule.term_rule, which tends to cause confusion due to builtin cterm_of (NB: the standard morphisms already provide a separate term component);

diff -r 8e8a339e176f -r b8920f3fd259 src/HOL/Tools/Function/function_common.ML
--- 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)
diff -r 8e8a339e176f -r b8920f3fd259 src/Pure/drule.ML
--- 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);