src/Pure/Isar/isar_syn.ML
changeset 17139 165c97f9bb63
parent 17107 2c35e00ee2ab
child 17142 76a5a2cc3171
--- a/src/Pure/Isar/isar_syn.ML	Wed Aug 24 12:05:48 2005 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Aug 24 12:07:00 2005 +0200
@@ -648,7 +648,8 @@
 val print_registrationsP =
   OuterSyntax.improper_command "print_interps"
     "print interpretations of named locale" K.diag
-    (P.xname >> (Toplevel.no_timing oo IsarCmd.print_registrations));
+    (Scan.optional (P.$$$ "!" >> K true) false -- P.xname >>
+      (Toplevel.no_timing oo uncurry IsarCmd.print_registrations));
 
 val print_attributesP =
   OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag