# HG changeset patch
# User wenzelm
# Date 1006617537 -3600
# Node ID c8214e408f35e4c29983d8c900feb9c2c643e7af
# Parent  7017cee2f3ac56c6cbead1819a74fc8020af3f23
print_locale: expr;

diff -r 7017cee2f3ac -r c8214e408f35 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sat Nov 24 16:58:31 2001 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Nov 24 16:58:57 2001 +0100
@@ -47,7 +47,7 @@
   val print_syntax: Toplevel.transition -> Toplevel.transition
   val print_theorems: Toplevel.transition -> Toplevel.transition
   val print_locales: Toplevel.transition -> Toplevel.transition
-  val print_locale: xstring -> Toplevel.transition -> Toplevel.transition
+  val print_locale: Locale.expr -> Toplevel.transition -> Toplevel.transition
   val print_attributes: Toplevel.transition -> Toplevel.transition
   val print_induct_rules: Toplevel.transition -> Toplevel.transition
   val print_trans_rules: Toplevel.transition -> Toplevel.transition
diff -r 7017cee2f3ac -r c8214e408f35 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Nov 24 16:58:31 2001 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sat Nov 24 16:58:57 2001 +0100
@@ -559,7 +559,7 @@
 
 val print_localeP =
   OuterSyntax.improper_command "print_locale" "print named locale of this theory" K.diag
-    (P.xname >> (Toplevel.no_timing oo IsarCmd.print_locale));
+    (P.locale_expr >> (Toplevel.no_timing oo IsarCmd.print_locale));
 
 val print_attributesP =
   OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag