--- a/src/HOL/Tools/datatype_package.ML Wed Mar 04 10:43:39 2009 +0100
+++ b/src/HOL/Tools/datatype_package.ML Wed Mar 04 10:45:52 2009 +0100
@@ -631,8 +631,8 @@
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
@@ -659,7 +659,7 @@
| 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)) ::