src/Pure/Isar/code.ML
changeset 51580 64ef8260dc60
parent 51551 88d1d19fb74f
child 51584 98029ceda8ce
     1.1 --- a/src/Pure/Isar/code.ML	Fri Mar 29 22:13:02 2013 +0100
     1.2 +++ b/src/Pure/Isar/code.ML	Fri Mar 29 22:14:27 2013 +0100
     1.3 @@ -955,9 +955,11 @@
     1.4      val exec = the_exec thy;
     1.5      fun pretty_equations const thms =
     1.6        (Pretty.block o Pretty.fbreaks) (
     1.7 -        Pretty.str (string_of_const thy const) :: map (Display.pretty_thm ctxt) thms
     1.8 +        Pretty.str (string_of_const thy const) ::
     1.9 +          map (Pretty.item o single o Display.pretty_thm ctxt) thms
    1.10        );
    1.11 -    fun pretty_function (const, Default (_, eqns_lazy)) = pretty_equations const (map fst (Lazy.force eqns_lazy))
    1.12 +    fun pretty_function (const, Default (_, eqns_lazy)) =
    1.13 +          pretty_equations const (map fst (Lazy.force eqns_lazy))
    1.14        | pretty_function (const, Eqns eqns) = pretty_equations const (map fst eqns)
    1.15        | pretty_function (const, Proj (proj, _)) = Pretty.block
    1.16            [Pretty.str (string_of_const thy const), Pretty.fbrk, Syntax.pretty_term ctxt proj]