# HG changeset patch
# User ballarin
# Date 1229523683 -3600
# Node ID db37b657a326828e43694a3cf3842e6c5e7d8047
# Parent  fa3fb943a0910d0f501bd15d15191cb765e8e761
Transfer theorems in print_locale.

diff -r fa3fb943a091 -r db37b657a326 src/Pure/Isar/new_locale.ML
--- a/src/Pure/Isar/new_locale.ML	Wed Dec 17 15:20:33 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML	Wed Dec 17 15:21:23 2008 +0100
@@ -375,8 +375,8 @@
     val ctxt = init name' thy
   in
     Pretty.big_list "locale elements:"
-      (activate_all name' thy (cons_elem show_facts) (K Morphism.identity) (empty, []) |>
-        snd |> rev |> 
+      (activate_all name' thy (cons_elem show_facts) (K (Element.transfer_morphism thy))
+        (empty, []) |> snd |> rev |> 
         map (Element.pretty_ctxt ctxt) |> map Pretty.chunks) |> Pretty.writeln
   end