src/Pure/Isar/locale.ML

--- a/src/Pure/Isar/locale.ML	Mon Aug 19 18:50:45 2013 +0200
+++ b/src/Pure/Isar/locale.ML	Mon Aug 19 20:37:36 2013 +0200
@@ -435,8 +435,6 @@
 
 (** Public activation functions **)
 
-fun transfer_morphism thy = Morphism.thm_morphism (Thm.transfer thy);
-
 fun activate_declarations dep = Context.proof_map (fn context =>
   let
     val thy = Context.theory_of context;
@@ -449,14 +447,15 @@
   let
     val thy = Context.theory_of context;
     val activate =
-      activate_notes Element.init (transfer_morphism o Context.theory_of) context export;
+      activate_notes Element.init
+        (Morphism.transfer_morphism o Context.theory_of) context export;
   in
     roundup thy activate (the_default Morphism.identity export) dep (Idents.get context, context)
     |-> Idents.put
   end;
 
 fun init name thy =
-  activate_all name thy Element.init (transfer_morphism o Context.theory_of)
+  activate_all name thy Element.init (Morphism.transfer_morphism o Context.theory_of)
     (empty_idents, Context.Proof (Proof_Context.init_global thy))
   |-> Idents.put |> Context.proof_of;
 
@@ -637,7 +636,7 @@
     fun cons_elem (elem as Notes _) = show_facts ? cons elem
       | cons_elem elem = cons elem;
     val elems =
-      activate_all name thy cons_elem (K (transfer_morphism thy)) (empty_idents, [])
+      activate_all name thy cons_elem (K (Morphism.transfer_morphism thy)) (empty_idents, [])
       |> snd |> rev;
   in
     Pretty.block