# HG changeset patch
# User wenzelm
# Date 1537383972 -7200
# Node ID 7d77eab54b178ceb39066a92cd3bb253c609889c
# Parent  0c1d7a414185624048ba4f90bdd7a907c02ff1a3
tuned;

diff -r 0c1d7a414185 -r 7d77eab54b17 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Wed Sep 19 20:45:47 2018 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Wed Sep 19 21:06:12 2018 +0200
@@ -609,7 +609,7 @@
   naming policy. Specifications in its body are inaccessible from outside.
   This is useful to perform experiments, without polluting the name space.
 
-  \<^descr> \<^theory_text>\<open>print_locale locale\<close> prints the contents of the named locale. The
+  \<^descr> \<^theory_text>\<open>print_locale "locale"\<close> prints the contents of the named locale. The
   command omits @{element "notes"} elements by default. Use \<^theory_text>\<open>print_locale!\<close>
   to have them included.