diff -r b2e1a7b83e05 -r 67370521c09c Nominal/nominal_function_common.ML
--- a/Nominal/nominal_function_common.ML	Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_function_common.ML	Thu Jul 09 02:32:46 2015 +0100
@@ -15,7 +15,7 @@
   defname : string,
     (* contains no logical entities: invariant under morphisms: *)
   add_simps : (binding -> binding) -> string -> (binding -> binding) ->
-    Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
+    Token.src list -> thm list -> local_theory -> thm list * local_theory,
   case_names : string list,
   fs : term list,
   R : term,
@@ -37,7 +37,7 @@
   defname : string,
     (* contains no logical entities: invariant under morphisms: *)
   add_simps : (binding -> binding) -> string -> (binding -> binding) ->
-    Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
+    Token.src list -> thm list -> local_theory -> thm list * local_theory,
   case_names : string list,
   fs : term list,
   R : term,
@@ -64,7 +64,7 @@
 structure NominalFunctionData = Generic_Data
 (
   type T = (term * nominal_info) Item_Net.T;
-  val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
+  val empty : T = Item_Net.init (op aconv o apply2 fst) (single o fst);
   val extend = I;
   fun merge tabs : T = Item_Net.merge tabs;
 )
@@ -72,9 +72,9 @@
 val get_function = NominalFunctionData.get o Context.Proof;
 
 
-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 (Thm.cterm_of ctxt t))
   in
     Morphism.morphism "lift_morphism"
       {binding = [],
@@ -85,12 +85,11 @@
 
 fun import_function_data t ctxt =
   let
-    val thy = Proof_Context.theory_of ctxt
-    val ct = cterm_of thy t
-    val inst_morph = lift_morphism thy o Thm.instantiate
+    val ct = Thm.cterm_of ctxt t
+    val inst_morph = lift_morphism ctxt o Thm.instantiate
 
     fun match (trm, data) =
-      SOME (morph_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct))))
+      SOME (morph_function_data data (inst_morph (Thm.match (Thm.cterm_of ctxt trm, ct))))
       handle Pattern.MATCH => NONE
   in
     get_first match (Item_Net.retrieve (get_function ctxt) t)