Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
print_locale: expr;
authorwenzelm
Sat, 24 Nov 2001 16:58:57 +0100
changeset 12288 c8214e408f35
parent 12287 7017cee2f3ac
child 12289 ec2dafd0a6a9
print_locale: expr;
src/Pure/Isar/isar_cmd.ML file | annotate | diff | comparison | revisions
src/Pure/Isar/isar_syn.ML file | annotate | diff | comparison | revisions 
--- 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
--- 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
isabelle