src/Pure/Isar/isar_syn.ML

   OuterSyntax.improper_command "print_locales" "print locales of this theory" K.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_locales));
 
 val print_localeP =
   OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag
-    (locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale));
+    (Scan.optional (P.$$$ "!" >> K true) false -- locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale));
 
 val print_registrationsP =
   OuterSyntax.improper_command "print_interps"
     "print interpretations of named locale" K.diag
     (Scan.optional (P.$$$ "!" >> K true) false -- P.xname >>