# HG changeset patch # User huffman # Date 1234555623 28800 # Node ID 333cbcad74c3dda842b4ae74f8447a42b0a9f08a # Parent c7328aa1b52ebb4c0498667d75bb76d1f3b32254# Parent 62390f5d0826fa4ae004c0a809d6ba6e9bdcc5a2 merged diff -r c7328aa1b52e -r 333cbcad74c3 src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Fri Feb 13 12:06:09 2009 -0800 +++ b/src/HOL/Tools/datatype_package.ML Fri Feb 13 12:07:03 2009 -0800 @@ -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; diff -r c7328aa1b52e -r 333cbcad74c3 src/Pure/General/seq.ML --- a/src/Pure/General/seq.ML Fri Feb 13 12:06:09 2009 -0800 +++ b/src/Pure/General/seq.ML Fri Feb 13 12:07:03 2009 -0800 @@ -89,17 +89,17 @@ (*the list of the first n elements, paired with rest of sequence; if length of list is less than n, then sequence had less than n elements*) fun chop n xq = - if n <= (0: int) then ([], xq) + if n <= (0 : int) then ([], xq) else (case pull xq of NONE => ([], xq) | SOME (x, xq') => apfst (Basics.cons x) (chop (n - 1) xq')); -(* truncate the sequence after n elements *) -fun take n s = let - fun f 0 _ () = NONE - | f n ss () = Option.map (apsnd (make o f (n - 1))) (pull ss); - in make (f n s) end; +(*truncate the sequence after n elements*) +fun take n xq = + if n <= (0 : int) then empty + else make (fn () => + (Option.map o apsnd) (take (n - 1)) (pull xq)); (*conversion from sequence to list*) fun list_of xq =