--- a/src/Pure/Isar/code.ML Sat Mar 30 12:13:39 2013 +0100
+++ b/src/Pure/Isar/code.ML Sat Mar 30 13:40:19 2013 +0100
@@ -954,10 +954,8 @@
val ctxt = Proof_Context.init_global thy;
val exec = the_exec thy;
fun pretty_equations const thms =
- (Pretty.block o Pretty.fbreaks) (
- Pretty.str (string_of_const thy const) ::
- map (Pretty.item o single o Display.pretty_thm ctxt) thms
- );
+ (Pretty.block o Pretty.fbreaks)
+ (Pretty.str (string_of_const thy const) :: map (Display.pretty_thm_item ctxt) thms);
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)