wenzelm [Thu, 22 Mar 2012 15:41:49 +0100] rev 47081
uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
uniform treatment of target contexts as invisible;
added Local_Theory.standard_form convenience;