Theory.thy

The type abbreviation thy_addon, declared as

   type thy_addon = {sig_ps : unit PP.pprinter option,
                     struct_ps : unit PP.pprinter option}

packages up the arguments to adjoin_to_theory. The sig_ps argument is an optional prettyprinter, which will be invoked when the theory signature file is written. The struct_ps argument is an optional prettyprinter invoked when the theory structure file is written.

The unit type parameter in both cases simply means that the pretty-printers won’t be passed any extra information when invoked.