# HG changeset patch
# User ballarin
# Date 1378239167 -7200
# Node ID 1f383542226b2f98f56dfa94b4438d200e4e5c5b
# Parent  c8c548d83862d5b0cbf3963067de1ea6ab3edc9b
New test case: interpretation in named contexts is not persistent.

diff -r c8c548d83862 -r 1f383542226b src/FOL/ex/Locale_Test/Locale_Test1.thy
--- 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