diff -r dd602eb20f3f -r 66cfe1d00be0 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Fri Jan 25 14:54:46 2008 +0100
+++ b/src/Pure/Isar/code.ML	Fri Jan 25 14:54:48 2008 +0100
@@ -450,6 +450,7 @@
                           :: Pretty.str "of" :: map (Pretty.quote o Sign.pretty_typ thy) tys)) cos)
           );
     val inlines = (#inlines o the_thmproc) exec;
+    val posts = (#posts o the_thmproc) exec;
     val inline_procs = (map fst o #inline_procs o the_thmproc) exec;
     val preprocs = (map fst o #preprocs o the_thmproc) exec;
     val funs = the_funcs exec
@@ -484,6 +485,11 @@
         :: (Pretty.fbreaks o map Pretty.str) preprocs
       ),
       Pretty.block (
+        Pretty.str "postprocessor theorems:"
+        :: Pretty.fbrk
+        :: (Pretty.fbreaks o map (ProofContext.pretty_thm ctxt)) posts
+      ),
+      Pretty.block (
         Pretty.str "datatypes:"
         :: Pretty.fbrk
         :: (Pretty.fbreaks o map pretty_dtyp) dtyps