Transfer morphism with theory closure.

--- a/src/Pure/Isar/element.ML	Tue Dec 16 15:08:08 2008 +0100
+++ b/src/Pure/Isar/element.ML	Tue Dec 16 20:18:46 2008 +0100
@@ -78,6 +78,7 @@
   val generalize_facts: Proof.context -> Proof.context ->
     (Attrib.binding * (thm list * Attrib.src list) list) list ->
     (Attrib.binding * (thm list * Attrib.src list) list) list
+  val transfer_morphism: theory -> morphism
   val activate: (typ, term, Facts.ref) ctxt list -> Proof.context -> context_i list * Proof.context
   val activate_i: context_i list -> Proof.context -> context_i list * Proof.context
 end;
@@ -537,6 +538,15 @@
   in facts_map (morph_ctxt morphism) facts end;
 
 
+(* transfer to theory using closure *)
+
+fun transfer_morphism thy =
+  let val thy_ref = Theory.check_thy thy in
+    Morphism.morphism {binding = I, var = I, typ = I, term = I,
+      fact = map (fn th => transfer (Theory.deref thy_ref) th)}
+  end;
+
+
 (** activate in context, return elements and facts **)
 
 local

--- a/src/Pure/Isar/new_locale.ML	Tue Dec 16 15:08:08 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML	Tue Dec 16 20:18:46 2008 +0100
@@ -292,8 +292,7 @@
     val Loc {notes, ...} = the_locale thy name;
     fun activate ((kind, facts), _) input =
       let
-        val facts' = facts |> Element.facts_map (Element.morph_ctxt
-          (Morphism.thm_morphism (transfer input) $> morph))
+        val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph))
       in activ_elem (Notes (kind, facts')) input end;
   in
     fold_rev activate notes input
@@ -355,17 +354,18 @@
   roundup thy activate_decls dep (get_local_idents ctxt, ctxt) |> uncurry put_local_idents;
 
 fun activate_global_facts dep thy =
-  roundup thy (activate_notes init_global_elem transfer) dep (get_global_idents thy, thy) |>
+  roundup thy (activate_notes init_global_elem Element.transfer_morphism)
+    dep (get_global_idents thy, thy) |>
   uncurry put_global_idents;
 
 fun activate_local_facts dep ctxt =
-  roundup (ProofContext.theory_of ctxt) (activate_notes init_local_elem
-      (transfer o ProofContext.theory_of)) dep
+  roundup (ProofContext.theory_of ctxt)
+  (activate_notes init_local_elem (Element.transfer_morphism o ProofContext.theory_of)) dep
     (get_local_idents ctxt, ctxt) |>
   uncurry put_local_idents;
 
 fun init name thy =
-  activate_all name thy init_local_elem (transfer o ProofContext.theory_of)
+  activate_all name thy init_local_elem (Element.transfer_morphism o ProofContext.theory_of)
     (empty, ProofContext.init thy) |>
   uncurry put_local_idents;
 
@@ -375,7 +375,8 @@
     val ctxt = init name' thy
   in
     Pretty.big_list "locale elements:"
-      (activate_all name' thy (cons_elem show_facts) (K I) (empty, []) |> snd |> rev |> 
+      (activate_all name' thy (cons_elem show_facts) (K Morphism.identity) (empty, []) |>
+        snd |> rev |> 
         map (Element.pretty_ctxt ctxt) |> map Pretty.chunks) |> Pretty.writeln
   end