more careful treatment of set_context / reset_context for persistent morphisms;
avoid persistent theory for eq_morphism / eq_term_morphism, notably in 'class' definition;

--- a/src/Pure/Isar/class.ML	Tue May 16 17:08:31 2023 +0200
+++ b/src/Pure/Isar/class.ML	Tue May 16 19:20:18 2023 +0200
@@ -157,8 +157,9 @@
 val base_morphism = #base_morph oo the_class_data;
 
 fun morphism thy class =
-  base_morphism thy class $>
-  Morphism.default (Element.eq_morphism thy (these_defs thy [class]));
+  Morphism.set_context thy
+   (base_morphism thy class $>
+    Morphism.default (Element.eq_morphism (these_defs thy [class])));
 
 val export_morphism = #export_morph oo the_class_data;
 
@@ -230,7 +231,7 @@
   in Class_Data.map add_class thy end;
 
 fun activate_defs class thms thy =
-  (case Element.eq_morphism thy thms of
+  (case Element.eq_morphism thms of
     SOME eq_morph =>
       fold (fn cls => fn thy' =>
         (Context.theory_map o Locale.amend_registration)
@@ -359,7 +360,8 @@
 
 fun target_const class phi0 prmode (b, rhs) lthy =
   let
-    val export = Variable.export_morphism lthy (Local_Theory.target_of lthy);
+    val export =
+      Morphism.set_context' lthy (Variable.export_morphism lthy (Local_Theory.target_of lthy));
     val guess_identity = guess_morphism_identity (b, rhs) export;
     val guess_canonical = guess_morphism_identity (b, rhs) (export $> phi0);
   in

--- a/src/Pure/Isar/class_declaration.ML	Tue May 16 17:08:31 2023 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Tue May 16 19:20:18 2023 +0200
@@ -74,7 +74,9 @@
     val base_morph = inst_morph
       $> Morphism.binding_morphism "class_binding" (Binding.prefix false (Class.class_prefix class))
       $> Element.satisfy_morphism (the_list some_witn);
-    val eq_morph = Element.eq_morphism thy (Class.these_defs thy sups |> map Thm.trim_context);
+    val eq_morph =
+      Element.eq_morphism (Class.these_defs thy sups)
+      |> Option.map (Morphism.set_context thy);
 
     (* assm_intro *)
     fun prove_assm_intro thm =

--- a/src/Pure/Isar/element.ML	Tue May 16 17:08:31 2023 +0200
+++ b/src/Pure/Isar/element.ML	Tue May 16 19:20:18 2023 +0200
@@ -51,8 +51,8 @@
   val pretty_witness: Proof.context -> witness -> Pretty.T
   val instantiate_normalize_morphism: ctyp TFrees.table * cterm Frees.table -> morphism
   val satisfy_morphism: witness list -> morphism
-  val eq_term_morphism: theory -> term list -> morphism option
-  val eq_morphism: theory -> thm list -> morphism option
+  val eq_term_morphism: term list -> morphism option
+  val eq_morphism: thm list -> morphism option
   val init: context_i -> Context.generic -> Context.generic
   val activate_i: context_i -> Proof.context -> context_i * Proof.context
   val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context
@@ -399,37 +399,42 @@
 (* rewriting with equalities *)
 
 (* for activating declarations only *)
-fun eq_term_morphism _ [] = NONE
-  | eq_term_morphism thy props =
+fun eq_term_morphism [] = NONE
+  | eq_term_morphism props =
       let
-        (* FIXME proper morphism context *)
-        fun decomp_simp prop =
+        fun decomp_simp ctxt prop =
           let
-            val ctxt = Proof_Context.init_global thy;
             val _ = Logic.no_prems prop orelse
               error ("Bad conditional rewrite rule " ^ Syntax.string_of_term ctxt prop);
-            val lhsrhs = Logic.dest_equals prop
-              handle TERM _ => error ("Rewrite rule not a meta-equality " ^ Syntax.string_of_term ctxt prop);
-          in lhsrhs end;
+          in
+            Logic.dest_equals prop handle TERM _ =>
+              error ("Rewrite rule not a meta-equality " ^ Syntax.string_of_term ctxt prop)
+          end;
+        fun rewrite_term thy =
+          let val ctxt = Proof_Context.init_global thy
+          in Pattern.rewrite_term thy (map (decomp_simp ctxt) props) [] end;
         val phi =
           Morphism.morphism "Element.eq_term_morphism"
            {binding = [],
             typ = [],
-            term = [K (Pattern.rewrite_term thy (map decomp_simp props) [])],
+            term = [rewrite_term o Morphism.the_theory],
             fact = [fn _ => fn _ => error "Illegal application of Element.eq_term_morphism"]};
       in SOME phi end;
 
-fun eq_morphism _ [] = NONE
-  | eq_morphism thy thms =
+fun eq_morphism [] = NONE
+  | eq_morphism thms =
       let
-        (* FIXME proper morphism context *)
-        fun rewrite th = rewrite_rule (Proof_Context.init_global (Thm.theory_of_thm th)) thms th;
+        val thms0 = map Thm.trim_context thms;
+        fun rewrite_term thy =
+          Raw_Simplifier.rewrite_term thy (map (Thm.transfer thy) thms0) [];
+        fun rewrite thy =
+          Raw_Simplifier.rewrite_rule (Proof_Context.init_global thy) (map (Thm.transfer thy) thms0);
         val phi =
           Morphism.morphism "Element.eq_morphism"
            {binding = [],
             typ = [],
-            term = [K (Raw_Simplifier.rewrite_term thy thms [])],
-            fact = [K (map rewrite)]};
+            term = [rewrite_term o Morphism.the_theory],
+            fact = [map o rewrite o Morphism.the_theory]};
       in SOME phi end;
 
 

--- a/src/Pure/Isar/expression.ML	Tue May 16 17:08:31 2023 +0200
+++ b/src/Pure/Isar/expression.ML	Tue May 16 19:20:18 2023 +0200
@@ -406,7 +406,7 @@
         val rewrite_morph = eqns'
           |> map (abs_def ctxt')
           |> Variable.export_terms ctxt' ctxt
-          |> Element.eq_term_morphism (Proof_Context.theory_of ctxt)
+          |> Element.eq_term_morphism
           |> Morphism.default;
        val ctxt'' = Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt;
        val eqnss' = eqnss @ [attrss ~~ Variable.export_terms ctxt' ctxt eqns'];

--- a/src/Pure/Isar/interpretation.ML	Tue May 16 17:08:31 2023 +0200
+++ b/src/Pure/Isar/interpretation.ML	Tue May 16 19:20:18 2023 +0200
@@ -111,9 +111,7 @@
     fun register (dep, eqns) ctxt =
       ctxt |> add_registration
         {inst = dep,
-          mixin =
-            Option.map (rpair true)
-              (Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns')),
+          mixin = Option.map (rpair true) (Element.eq_morphism (eqns @ eqns')),
           export = export};
   in ctxt'' |> fold register (deps' ~~ eqnss') end;
 

--- a/src/Pure/Isar/locale.ML	Tue May 16 17:08:31 2023 +0200
+++ b/src/Pure/Isar/locale.ML	Tue May 16 19:20:18 2023 +0200
@@ -107,8 +107,14 @@
 type dep = {name: string, morphisms: morphism * morphism, pos: Position.T, serial: serial};
 fun eq_dep (dep1: dep, dep2: dep) = #serial dep1 = #serial dep2;
 
+fun transfer_dep thy ({name, morphisms, pos, serial}: dep) : dep =
+  {name = name, morphisms = apply2 (Morphism.set_context thy) morphisms, pos = pos, serial = serial};
+
 fun make_dep (name, morphisms) : dep =
-  {name = name, morphisms = morphisms, pos = Position.thread_data (), serial = serial ()};
+ {name = name,
+  morphisms = apply2 Morphism.reset_context morphisms,
+  pos = Position.thread_data (),
+  serial = serial ()};
 
 (*table of mixin lists, per list mixins in reverse order of declaration;
   lists indexed by registration/dependency serial,
@@ -120,7 +126,8 @@
 
 val merge_mixins: mixins * mixins -> mixins = Inttab.merge_list (eq_snd op =);
 
-fun insert_mixin serial' mixin : mixins -> mixins = Inttab.cons_list (serial', (mixin, serial ()));
+fun insert_mixin serial' (morph, b) : mixins -> mixins =
+  Inttab.cons_list (serial', ((Morphism.reset_context morph, b), serial ()));
 
 fun rename_mixin (old, new) (mixins: mixins) =
   (case Inttab.lookup mixins old of
@@ -216,8 +223,7 @@
           map Element.trim_context_ctxt hyp_spec),
         ((map (fn decl => (decl, serial ())) syntax_decls,
           map (fn (a, facts) => ((a, map Attrib.trim_context_fact facts), serial ())) notes),
-          (map (fn (name, morph) =>
-                make_dep (name, (Morphism.reset_context morph, Morphism.identity))) dependencies,
+          (map (fn (name, morph) => make_dep (name, (morph, Morphism.identity))) dependencies,
             Inttab.empty)))) #> snd);
           (* FIXME Morphism.identity *)
 
@@ -236,15 +242,17 @@
 fun axioms_of thy = map (Thm.transfer thy) o #axioms o the_locale thy;
 
 fun instance_of thy name morph = params_of thy name |>
-  map (Morphism.term morph o Free o #1);
+  map (Morphism.term (Morphism.set_context thy morph) o Free o #1);
 
 fun specification_of thy = #spec o the_locale thy;
 
-fun hyp_spec_of thy = #hyp_spec o the_locale thy;
+fun hyp_spec_of thy = map (Element.transfer_ctxt thy) o #hyp_spec o the_locale thy;
+
+fun dependencies_of thy = map (transfer_dep thy) o #dependencies o the_locale thy;
 
-fun dependencies_of thy = #dependencies o the_locale thy;
-
-fun mixins_of thy name serial = lookup_mixins (#mixins (the_locale thy name)) serial;
+fun mixins_of thy name serial =
+  lookup_mixins (#mixins (the_locale thy name)) serial
+  |> (map o apfst o apfst) (Morphism.set_context thy);
 
 
 (* Print instance and qualifiers *)
@@ -398,7 +406,10 @@
 
 fun add_reg thy export (name, morph) =
   let
-    val reg = {morphisms = (morph, export), pos = Position.thread_data (), serial = serial ()};
+    val reg =
+     {morphisms = (Morphism.reset_context morph, Morphism.reset_context export),
+      pos = Position.thread_data (),
+      serial = serial ()};
     val id = (name, instance_of thy name (morph $> export));
   in (map_registrations o apfst) (Idtab.insert (K false) (id, reg)) end;
 
@@ -494,28 +505,28 @@
       handle ERROR msg => activate_err msg "syntax" (name, morph) context
   end;
 
-fun activate_notes activ_elem transfer context export' (name, morph) input =
+fun activate_notes activ_elem context export' (name, morph) input =
   let
     val thy = Context.theory_of context;
     val mixin =
       (case export' of
         NONE => Morphism.identity
       | SOME export => collect_mixins context (name, morph $> export) $> export);
-    val morph' = transfer input $> morph $> mixin;
+    val morph' = Morphism.set_context thy (morph $> mixin);
     val notes' = map (Element.transform_ctxt morph') (lazy_notes thy name);
   in
     (notes', input) |-> fold (fn elem => fn res =>
-      activ_elem (Element.transform_ctxt (transfer res) elem) res)
+      activ_elem (Element.transfer_ctxt thy elem) res)
   end handle ERROR msg => activate_err msg "facts" (name, morph) context;
 
-fun activate_notes_trace activ_elem transfer context export' (name, morph) context' =
+fun activate_notes_trace activ_elem context export' (name, morph) context' =
   let
     val _ = trace "facts" (name, morph) context';
   in
-    activate_notes activ_elem transfer context export' (name, morph) context'
+    activate_notes activ_elem context export' (name, morph) context'
   end;
 
-fun activate_all name thy activ_elem transfer (marked, input) =
+fun activate_all name thy activ_elem (marked, input) =
   let
     val {parameters = (_, params), spec = (asm, defs), ...} = the_locale thy name;
     val input' = input |>
@@ -525,7 +536,7 @@
       (case asm of SOME A => activ_elem (Assumes [(Binding.empty_atts, [(A, [])])]) | _ => I) |>
       (not (null defs) ?
         activ_elem (Defines (map (fn def => (Binding.empty_atts, (def, []))) defs)));
-    val activate = activate_notes activ_elem transfer (Context.Theory thy) NONE;
+    val activate = activate_notes activ_elem (Context.Theory thy) NONE;
   in
     roundup thy activate Morphism.identity (name, Morphism.identity) (marked, input')
   end;
@@ -538,7 +549,7 @@
   |> Context_Position.set_visible_generic false
   |> pair (Idents.get context)
   |> roundup (Context.theory_of context)
-      (activate_notes_trace init_element Morphism.transfer_morphism'' context export)
+      (activate_notes_trace init_element context export)
       (Morphism.default export) dep
   |-> Idents.put
   |> Context_Position.restore_visible_generic context;
@@ -559,7 +570,7 @@
     context
     |> Context_Position.set_visible_generic false
     |> pair empty_idents
-    |> activate_all name thy init_element Morphism.transfer_morphism''
+    |> activate_all name thy init_element
     |-> (fn marked' => Idents.put (merge_idents (marked, marked')))
     |> Context_Position.restore_visible_generic context
     |> Context.proof_of
@@ -735,7 +746,7 @@
       | cons_elem (elem as Lazy_Notes _) = show_facts ? cons elem
       | cons_elem elem = cons elem;
     val elems =
-      activate_all name thy cons_elem (K (Morphism.transfer_morphism thy)) (empty_idents, [])
+      activate_all name thy cons_elem (empty_idents, [])
       |> snd |> rev
       |> tap consolidate_notes
       |> map force_notes;