src/Pure/Isar/new_locale.ML
changeset 29220 db37b657a326
parent 29218 f7ffe90879e2
child 29222 1ec081e2eae9
--- 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