# HG changeset patch
# User haftmann
# Date 1236170519 -3600
# Node ID 4f699164ab0c3a367260455b95a951cbf2631180
# Parent  8c2649eb6a208966fe14c3a2a03c4b01b982e918
datatype antiquotation does not assume LaTeX as output any longer

diff -r 8c2649eb6a20 -r 4f699164ab0c src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Wed Mar 04 11:49:12 2009 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Wed Mar 04 13:41:59 2009 +0100
@@ -629,14 +629,6 @@
 
 (** a datatype antiquotation **)
 
-local
-
-val sym_datatype = Pretty.command "datatype";
-val sym_binder = Pretty.str "\\ {\\isacharequal}"; (*FIXME use proper symbol*)
-val sym_sep = Pretty.str "{\\isacharbar}\\ ";
-
-in
-
 fun args_datatype (ctxt, args) =
   let
     val (tyco, (ctxt', args')) = Args.tyname (ctxt, args);
@@ -654,26 +646,19 @@
       in if member (op =) s " " then Pretty.enclose "(" ")" [p]
         else p
       end;
-    fun pretty_constr (co, []) =
-          Syntax.pretty_term ctxt (Const (co, ty))
-      | pretty_constr (co, [ty']) =
-          (Pretty.block o Pretty.breaks)
-            [Syntax.pretty_term ctxt (Const (co, ty' --> ty)),
-              pretty_typ_br ty']
-      | pretty_constr (co, tys) =
-          (Pretty.block o Pretty.breaks)
-            (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
-              map pretty_typ_br tys);
+    fun pretty_constr (co, tys) =
+      (Pretty.block o Pretty.breaks)
+        (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
+          map pretty_typ_br tys);
   in
     Pretty.block
-      (sym_datatype :: Pretty.brk 1 ::
+      (Pretty.command "datatype" :: Pretty.brk 1 ::
        Syntax.pretty_typ ctxt ty ::
-       sym_binder :: Pretty.brk 1 ::
-       flat (separate [Pretty.brk 1, sym_sep]
+       Pretty.str " =" :: Pretty.brk 1 ::
+       flat (separate [Pretty.brk 1, Pretty.str "| "]
          (map (single o pretty_constr) cos)))
   end
 
-end;
 
 (** package setup **)