src/HOL/Tools/datatype_package.ML

 
 (** a datatype antiquotation **)
 
 local
 
-val sym_datatype = Pretty.str "\\isacommand{datatype}";
-val sym_binder = Pretty.str "\\ {\\isacharequal}";
+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) =

     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)),
-              Syntax.pretty_typ ctxt 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);
   in