Local_Theory.map_contexts with explicit level indication: 0 = main target at bottom;
Local_Theory.target refers to bottom;
tuned signature;
use_thys [
"Auth_Shared",
"Auth_Public",
"Smartcard/Auth_Smartcard",
"Guard/Auth_Guard_Shared",
"Guard/Auth_Guard_Public"
];