# HG changeset patch
# User berghofe
# Date 1234540028 -3600
# Node ID 62390f5d0826fa4ae004c0a809d6ba6e9bdcc5a2
# Parent  9049a2bfbe6d1ff10aaeeebdc94ab6741ecb9901
Tuned datatype antiquotation.

diff -r 9049a2bfbe6d -r 62390f5d0826 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Fri Feb 13 13:28:14 2009 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Fri Feb 13 16:47:08 2009 +0100
@@ -632,9 +632,8 @@
 local
 
 val sym_datatype = Pretty.str "\\isacommand{datatype}";
-val sym_binder = Pretty.str "{\\isacharequal}";
-val sym_of = Pretty.str "of";
-val sym_sep = Pretty.str "{\\isacharbar}";
+val sym_binder = Pretty.str "\\ {\\isacharequal}";
+val sym_sep = Pretty.str "{\\isacharbar}\\ ";
 
 in
 
@@ -660,17 +659,19 @@
       | pretty_constr (co, [ty']) =
           (Pretty.block o Pretty.breaks)
             [Syntax.pretty_term ctxt (Const (co, ty' --> ty)),
-              sym_of, Syntax.pretty_typ ctxt ty']
+              Syntax.pretty_typ ctxt ty']
       | pretty_constr (co, tys) =
           (Pretty.block o Pretty.breaks)
             (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
-              sym_of :: map pretty_typ_br tys);
-  in (Pretty.block o Pretty.breaks) (
-    sym_datatype
-    :: Syntax.pretty_typ ctxt ty
-    :: sym_binder
-    :: separate sym_sep (map pretty_constr cos)
-  ) end
+              map pretty_typ_br tys);
+  in
+    Pretty.block
+      (sym_datatype :: Pretty.brk 1 ::
+       Syntax.pretty_typ ctxt ty ::
+       sym_binder :: Pretty.brk 1 ::
+       flat (separate [Pretty.brk 1, sym_sep]
+         (map (single o pretty_constr) cos)))
+  end
 
 end;