diff -r dc8a41c7cefc -r 8665d08085df src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Mar 08 16:02:52 2005 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Mar 09 18:44:52 2005 +0100
@@ -49,6 +49,7 @@
   val print_locales: Toplevel.transition -> Toplevel.transition
   val print_locale: Locale.expr * Args.src Locale.element list
     -> Toplevel.transition -> Toplevel.transition
+  val print_registrations: string -> Toplevel.transition -> Toplevel.transition
   val print_attributes: Toplevel.transition -> Toplevel.transition
   val print_rules: Toplevel.transition -> Toplevel.transition
   val print_induct_rules: Toplevel.transition -> Toplevel.transition
@@ -218,7 +219,12 @@
 
 fun print_locale (import, body) = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   let val thy = Toplevel.theory_of state in
-    Locale.print_locale thy import (map (Locale.map_attrib_element (Attrib.local_attribute thy)) body)
+    Locale.print_locale thy import (map (Locale.map_attrib_element (Attrib.multi_attribute thy)) body)
+  end);
+
+fun print_registrations name = Toplevel.unknown_theory o
+  Toplevel.keep (fn state => let val thy = Toplevel.theory_of state in
+    Locale.print_global_registrations thy name
   end);
 
 val print_attributes = Toplevel.unknown_theory o