fixed soundness bug in Nitpick related to unfolding -- the unfolding criterion must at least as strict when looking at a definitional axiom as elsewhere, otherwise we end up unfolding a constant's definition in its own definition, yielding a trivial equality

more robust Swing_Thread.now: allow body to fail;

tuned proofs;

reparse descendants after update of imports, e.g. required for 'primrec' (line 17 of "src/HOL/Power.thy");