We have a problem with PAPP_Impossibility for quite some time. I am presently running a bisection to see better where it actually happens: presently the interval is Isabelle/f5aca3ed1adb .. 69ee23f83884 based on https://isabelle.sketis.net/devel/build_status/AFP/PAPP_Impossibility.csv Stay tuned ... Makarius