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

     2.1 --- a/src/Pure/drule.ML	Wed Feb 15 21:38:28 2012 +0100
     2.2 +++ b/src/Pure/drule.ML	Wed Feb 15 22:44:31 2012 +0100
     2.3 @@ -95,7 +95,6 @@
     2.4    val mk_term: cterm -> thm
     2.5    val dest_term: thm -> cterm
     2.6    val cterm_rule: (thm -> thm) -> cterm -> cterm
     2.7 -  val term_rule: theory -> (thm -> thm) -> term -> term
     2.8    val dummy_thm: thm
     2.9    val sort_constraintI: thm
    2.10    val sort_constraint_eq: thm
    2.11 @@ -720,7 +719,6 @@
    2.12    end;
    2.13  
    2.14  fun cterm_rule f = dest_term o f o mk_term;
    2.15 -fun term_rule thy f t = Thm.term_of (cterm_rule f (Thm.cterm_of thy t));
    2.16  
    2.17  val dummy_thm = mk_term (certify Term.dummy_prop);
    2.18