Transfer theorems in print_locale.
--- 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