# HG changeset patch
# User wenzelm
# Date 1684446659 -7200
# Node ID 15ab739497134da2a3aa069023cfe8166a1e4e5a
# Parent  073826f50e146ec7f2fbc28d3cc8f5e522f7782b
more careful reset/set_context for stored declarations;

diff -r 073826f50e14 -r 15ab73949713 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu May 18 23:21:05 2023 +0200
+++ b/src/Pure/Isar/locale.ML	Thu May 18 23:50:59 2023 +0200
@@ -221,7 +221,7 @@
       mk_locale ((parameters, spec, (apply2 o Option.map) Thm.trim_context intros,
           map Thm.trim_context axioms,
           map Element.trim_context_ctxt hyp_spec),
-        ((map (fn decl => (decl, serial ())) syntax_decls,
+        ((map (fn decl => (Morphism.entity_reset_context decl, serial ())) syntax_decls,
           map (fn (a, facts) => ((a, map Attrib.trim_context_fact facts), serial ())) notes),
           (map (fn (name, morph) => make_dep (name, (morph, Morphism.identity))) dependencies,
             Inttab.empty)))) #> snd);
@@ -499,9 +499,10 @@
     val _ = trace "syntax" (name, morph) context;
     val thy = Context.theory_of context;
     val {syntax_decls, ...} = the_locale thy name;
+    val form_syntax_decl =
+      Morphism.form o Morphism.transform morph o Morphism.entity_set_context thy;
   in
-    context
-    |> fold_rev (Morphism.form o Morphism.transform morph o #1) syntax_decls
+    fold_rev (form_syntax_decl o #1) syntax_decls context
       handle ERROR msg => activate_err msg "syntax" (name, morph) context
   end;
 
@@ -674,9 +675,11 @@
     end;
 
 fun add_declaration loc syntax decl =
-  syntax ?
-    Proof_Context.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
-  #> add_facts loc "" [(Binding.empty_atts, Attrib.internal_declaration decl)];
+  let val decl0 = Morphism.entity_reset_context decl in
+    syntax ?
+      Proof_Context.background_theory ((change_locale loc o apfst o apfst) (cons (decl0, serial ())))
+    #> add_facts loc "" [(Binding.empty_atts, Attrib.internal_declaration decl0)]
+  end;
 
 
 (*** Reasoning about locales ***)
diff -r 073826f50e14 -r 15ab73949713 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Thu May 18 23:21:05 2023 +0200
+++ b/src/Pure/Isar/token.ML	Thu May 18 23:50:59 2023 +0200
@@ -490,19 +490,26 @@
 
 local
 
-fun context thm_context morphism_context =
+fun context thm_context morphism_context attribute_context declaration_context =
   let
     fun token_context tok = map_value
       (fn Source src => Source (map token_context src)
         | Fact (a, ths) => Fact (a, map thm_context ths)
         | Name (a, phi) => Name (a, morphism_context phi)
+        | Attribute a => Attribute (attribute_context a)
+        | Declaration a => Declaration (declaration_context a)
         | v => v) tok;
   in token_context end;
 
 in
 
-val trim_context = context Thm.trim_context Morphism.reset_context;
-fun transfer thy = context (Thm.transfer thy) (Morphism.set_context thy);
+val trim_context =
+  context Thm.trim_context Morphism.reset_context
+    Morphism.entity_reset_context Morphism.entity_reset_context;
+
+fun transfer thy =
+  context (Thm.transfer thy) (Morphism.set_context thy)
+    (Morphism.entity_set_context thy) (Morphism.entity_set_context thy);
 
 end;
 
diff -r 073826f50e14 -r 15ab73949713 src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Thu May 18 23:21:05 2023 +0200
+++ b/src/Pure/morphism.ML	Thu May 18 23:50:59 2023 +0200
@@ -41,6 +41,10 @@
   val compose: morphism -> morphism -> morphism
   type 'a entity
   val entity: (morphism -> 'a) -> 'a entity
+  val entity_reset_context: 'a entity -> 'a entity
+  val entity_set_context: theory -> 'a entity -> 'a entity
+  val entity_set_context': Proof.context -> 'a entity -> 'a entity
+  val entity_set_context'': Context.generic -> 'a entity -> 'a entity
   val transform: morphism -> 'a entity -> 'a entity
   val form: 'a entity -> 'a
   val form_entity: (morphism -> 'a) -> 'a
@@ -171,11 +175,18 @@
 
 (* abstract entities *)
 
-datatype 'a entity = Entity of morphism -> 'a
-fun entity f = Entity f;
+datatype 'a entity = Entity of (morphism -> 'a) * morphism;
+fun entity f = Entity (f, identity);
 
-fun transform phi (Entity f) = Entity (fn psi => f (phi $> psi));
-fun form (Entity f) = f identity;
+fun entity_morphism g (Entity (f, phi)) = Entity (f, g phi);
+fun entity_reset_context a = entity_morphism reset_context a;
+fun entity_set_context thy a = entity_morphism (set_context thy) a;
+fun entity_set_context' ctxt a = entity_morphism (set_context' ctxt) a;
+fun entity_set_context'' context a = entity_morphism (set_context'' context) a;
+
+fun transform phi2 (Entity (f, phi1)) = Entity (f, phi1 $> phi2);
+fun form (Entity (f, phi)) = f phi;
+
 fun form_entity f = f identity;
 
 type declaration = (Context.generic -> Context.generic) entity;