diff -r b60e65ad13df -r e6939796717e src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Fri Mar 06 00:00:57 2015 +0100
+++ b/src/HOL/Tools/Function/function_common.ML	Fri Mar 06 13:39:34 2015 +0100
@@ -325,9 +325,9 @@
         elims = Option.map (map fact) elims, pelims = map fact pelims }
     end
 
-fun lift_morphism thy f =
+fun lift_morphism ctxt f =
   let
-    fun term t = Thm.term_of (Drule.cterm_rule f (Thm.cterm_of thy t))
+    fun term t = Thm.term_of (Drule.cterm_rule f (Proof_Context.cterm_of ctxt t))
   in
     Morphism.morphism "lift_morphism"
       {binding = [],
@@ -338,13 +338,12 @@
 
 fun import_function_data t ctxt =
   let
-    val thy = Proof_Context.theory_of ctxt
-    val ct = Thm.cterm_of thy t
-    val inst_morph = lift_morphism thy o Thm.instantiate
+    val ct = Proof_Context.cterm_of ctxt t
+    val inst_morph = lift_morphism ctxt o Thm.instantiate
 
     fun match (trm, data) =
-      SOME (transform_function_data data (inst_morph (Thm.match (Thm.cterm_of thy trm, ct))))
-      handle Pattern.MATCH => NONE
+      SOME (transform_function_data data (inst_morph (Thm.match (Proof_Context.cterm_of ctxt trm, ct))))
+        handle Pattern.MATCH => NONE
   in
     get_first match (Item_Net.retrieve (get_functions ctxt) t)
   end