# 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 =