On Mon, 14 Nov 2011, Andreas Schropp wrote: > But > > fun add_non_pervasive_declaration decl lthy = > lthy > |> Local_Theory.declaration false decl > |> Context.proof_map (Morphism.form decl) > > should do the job based on Isabelle2011-1's Local_Theory.declaration? Yes, this is right. Makarius