more robust Thm.expose_theory -- ensure that PIDE export happens in the proper theory context;