--- 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.