workaround to avoid subtle "add_ffpairs" unification exception in Sledgehammer;
to reproduce the old bug, replace the command
by(rule new_Addr_SomeD)
on line 27 of Jinja/J/TypeSafe.thy with
by (metis new_Addr_SomeD)
s/\\([a-zA-Z]+)\s*/$1/g;
s/\$//g;
s/^BOOKMARK/\\BOOKMARK/g;