diff -r ec3b78ce0758 -r 64ef8260dc60 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Fri Mar 29 22:13:02 2013 +0100
+++ b/src/Pure/Isar/code.ML	Fri Mar 29 22:14:27 2013 +0100
@@ -955,9 +955,11 @@
     val exec = the_exec thy;
     fun pretty_equations const thms =
       (Pretty.block o Pretty.fbreaks) (
-        Pretty.str (string_of_const thy const) :: map (Display.pretty_thm ctxt) thms
+        Pretty.str (string_of_const thy const) ::
+          map (Pretty.item o single o Display.pretty_thm ctxt) thms
       );
-    fun pretty_function (const, Default (_, eqns_lazy)) = pretty_equations const (map fst (Lazy.force eqns_lazy))
+    fun pretty_function (const, Default (_, eqns_lazy)) =
+          pretty_equations const (map fst (Lazy.force eqns_lazy))
       | pretty_function (const, Eqns eqns) = pretty_equations const (map fst eqns)
       | pretty_function (const, Proj (proj, _)) = Pretty.block
           [Pretty.str (string_of_const thy const), Pretty.fbrk, Syntax.pretty_term ctxt proj]