# HG changeset patch
# User wenzelm
# Date 1553775657 -3600
# Node ID 063da22e1c9e8b57cf2c6138d3b22822a99c810f
# Parent  f12a52b5d81230f6bf72f6e90eb877bf310886b6
clarified diagrams;

diff -r f12a52b5d812 -r 063da22e1c9e src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Mar 28 13:06:32 2019 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Mar 28 13:20:57 2019 +0100
@@ -2345,9 +2345,12 @@
       ('(' target ')' '-' ? + @'and')
     ;
     printing_module: symbol_module ('\<rightharpoonup>' | '=>') \<newline>
-      ('(' target ')' \<newline>
-        (@{syntax string}
-          (@'for' ((symbol_const | symbol_type_constructor | symbol_class | symbol_class_relation | symbol_class_instance)+))?)? + @'and')
+      ('(' target ')' (@{syntax string} for_symbol?)? + @'and')
+    ;
+    for_symbol:
+      @'for'
+        ((symbol_const | symbol_typeconstructor |
+          symbol_class | symbol_class_relation | symbol_class_instance)+)
     ;
     @@{command (HOL) code_printing} ((printing_const | printing_type_constructor
       | printing_class | printing_class_relation | printing_class_instance