New test case: interpretation in named contexts is not persistent.

--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Tue Sep 03 22:12:47 2013 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Tue Sep 03 22:12:47 2013 +0200
@@ -768,6 +768,23 @@
 lemma (in roundup) "True & True <-> True" by (rule sub.true)
 
 
+section {* Interpretation in named contexts *}
+
+locale container
+begin
+interpretation private!: roundup True by unfold_locales rule
+lemmas true_copy = private.true
+end
+
+context container begin
+ML {* (Context.>> (fn generic => let val context = Context.proof_of generic
+  val _ = Proof_Context.get_thms context "private.true" in generic end);
+  error "thm private.true was persisted")
+  handle ERROR "Unknown fact \"private.true\"" => ([]:thm list); *}
+thm true_copy
+end
+
+
 section {* Interpretation in proofs *}
 
 lemma True