src/Pure/Pure.thy

       Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_locales\<close>
     "print locales of this theory"
-    (Parse.opt_bang >> (fn b =>
-      Toplevel.keep (Locale.print_locales b o Toplevel.theory_of)));
+    (Parse.opt_bang >> (fn verbose =>
+      Toplevel.keep (fn state =>
+        let val thy = Toplevel.theory_of state
+        in Pretty.writeln (Locale.pretty_locales thy verbose) end)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_classes\<close>
     "print classes of this theory"
     (Scan.succeed (Toplevel.keep (Class.print_classes o Toplevel.context_of)));

         in Pretty.writeln (Locale.pretty_locale thy show_facts name) end)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_interps\<close>
     "print interpretations of locale for this theory or proof context"
-    (Parse.position Parse.name >> (fn name =>
-      Toplevel.keep (fn state => Locale.print_registrations (Toplevel.context_of state) name)));
+    (Parse.position Parse.name >> (fn raw_name =>
+      Toplevel.keep (fn state =>
+        let
+          val ctxt = Toplevel.context_of state;
+          val thy = Toplevel.theory_of state;
+          val name = Locale.check thy raw_name;
+        in Pretty.writeln (Locale.pretty_registrations ctxt name) end)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_dependencies\<close>
     "print dependencies of locale expression"
     (Parse.opt_bang -- Parse_Spec.locale_expression >> (fn (clean, expr) =>