src/Tools/code/code_ml.ML
changeset 31665 a1f4d3b3f6c8
parent 31598 946a7a175bf1
child 31724 9b5a128cdb5c
--- a/src/Tools/code/code_ml.ML	Mon Jun 15 16:13:19 2009 +0200
+++ b/src/Tools/code/code_ml.ML	Tue Jun 16 14:56:59 2009 +0200
@@ -151,7 +151,7 @@
                 concat [str delim, p, str "=>", pr_term is_closure thm vars' NOBR body]
               end;
           in
-            (Pretty.enclose "(" ")" o single o brackify fxy) (
+            brackets (
               str "case"
               :: pr_term is_closure thm vars NOBR t
               :: pr "of" clause
@@ -441,8 +441,10 @@
               |>> (fn p => concat
                   [str "let", p, str "=", pr_term is_closure thm vars NOBR t, str "in"])
             val (ps, vars') = fold_map pr binds vars;
-            fun mk_brack (p :: ps) = Pretty.block [str "(", p] :: ps;
-          in Pretty.chunks (mk_brack ps @| Pretty.block [pr_term is_closure thm vars' NOBR body, str ")"]) end
+          in
+            brackify_block fxy (Pretty.chunks ps) []
+              (pr_term is_closure thm vars' NOBR body)
+          end
       | pr_case is_closure thm vars fxy (((t, ty), clause :: clauses), _) =
           let
             fun pr delim (pat, body) =
@@ -450,7 +452,7 @@
                 val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars;
               in concat [str delim, p, str "->", pr_term is_closure thm vars' NOBR body] end;
           in
-            (Pretty.enclose "(" ")" o single o brackify fxy) (
+            brackets (
               str "match"
               :: pr_term is_closure thm vars NOBR t
               :: pr "with" clause