Transfer theorems in print_locale.
authorballarin
Wed, 17 Dec 2008 15:21:23 +0100
changeset 29220 db37b657a326
parent 29219 fa3fb943a091
child 29221 918687637307
Transfer theorems in print_locale.
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