diff -r 8e5072cba671 -r 774752af4a1f src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Sun Sep 06 22:14:52 2015 +0200
+++ b/src/Tools/Code/code_ml.ML	Sun Sep 06 22:14:52 2015 +0200
@@ -454,8 +454,7 @@
                   [str "let", p, str "=", print_term is_pseudo_fun some_thm vars NOBR t, str "in"])
             val (ps, vars') = fold_map print_let binds vars;
           in
-            brackify_block fxy (Pretty.chunks ps) []
-              (print_term is_pseudo_fun some_thm vars' NOBR body)
+            brackets [Pretty.chunks ps, print_term is_pseudo_fun some_thm vars' NOBR body]
           end
       | print_case is_pseudo_fun some_thm vars fxy { term = t, typ = ty, clauses = clause :: clauses, ... } =
           let