src/Pure/Isar/code.ML
changeset 25968 66cfe1d00be0
parent 25597 34860182b250
child 26021 25d06476727e
     1.1 --- a/src/Pure/Isar/code.ML	Fri Jan 25 14:54:46 2008 +0100
     1.2 +++ b/src/Pure/Isar/code.ML	Fri Jan 25 14:54:48 2008 +0100
     1.3 @@ -450,6 +450,7 @@
     1.4                            :: Pretty.str "of" :: map (Pretty.quote o Sign.pretty_typ thy) tys)) cos)
     1.5            );
     1.6      val inlines = (#inlines o the_thmproc) exec;
     1.7 +    val posts = (#posts o the_thmproc) exec;
     1.8      val inline_procs = (map fst o #inline_procs o the_thmproc) exec;
     1.9      val preprocs = (map fst o #preprocs o the_thmproc) exec;
    1.10      val funs = the_funcs exec
    1.11 @@ -484,6 +485,11 @@
    1.12          :: (Pretty.fbreaks o map Pretty.str) preprocs
    1.13        ),
    1.14        Pretty.block (
    1.15 +        Pretty.str "postprocessor theorems:"
    1.16 +        :: Pretty.fbrk
    1.17 +        :: (Pretty.fbreaks o map (ProofContext.pretty_thm ctxt)) posts
    1.18 +      ),
    1.19 +      Pretty.block (
    1.20          Pretty.str "datatypes:"
    1.21          :: Pretty.fbrk
    1.22          :: (Pretty.fbreaks o map pretty_dtyp) dtyps