src/Pure/codegen.ML

 in
   val _ = Context.add_setup (add_simple_attribute ("unfold",
     fn thm => add_unfold thm #> CodeData.add_inline thm));
   val _ = map (Context.add_setup o add_del_attribute) [
     ("func", (CodeData.add_func true, CodeData.del_func)),
-    ("inline", (CodeData.add_inline, CodeData.del_inline))
+    ("inline", (CodeData.add_inline, CodeData.del_inline)),
+    ("post", (CodeData.add_post, CodeData.del_post))
   ];
 end; (*local*)
 
 
 (**** associate constants with target language code ****)