# HG changeset patch
# User wenzelm
# Date 1684249711 -7200
# Node ID 4e865c45458bf68d5cacb0848876241e76fe60f6
# Parent  7c9f290dff5514f1a97677f926f68dc891fc5b27
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
clarified signature;

diff -r 7c9f290dff55 -r 4e865c45458b src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue May 16 15:15:56 2023 +0200
+++ b/src/Pure/Isar/attrib.ML	Tue May 16 17:08:31 2023 +0200
@@ -187,12 +187,19 @@
 fun map_facts_refs f g = map_facts f #> map (apsnd (map (apfst g)));
 
 
-(* fact expressions *)
+(* implicit context *)
+
+val trim_context_binding: Attrib.binding -> Attrib.binding =
+  apsnd ((map o map) Token.trim_context);
 
-val trim_context_binding: Attrib.binding -> Attrib.binding = apsnd (map Token.trim_context_src);
-val trim_context_thms: thms -> thms = (map o apfst o map) Thm.trim_context;
+val trim_context_thms: thms -> thms =
+  map (fn (thms, atts) => (map Thm.trim_context thms, (map o map) Token.trim_context atts));
+
 fun trim_context_fact (binding, thms) = (trim_context_binding binding, trim_context_thms thms);
 
+
+(* fact expressions *)
+
 fun global_notes kind facts thy = thy |>
   Global_Theory.note_thmss kind (map_facts (map (attribute_global thy)) facts);
 
diff -r 7c9f290dff55 -r 4e865c45458b src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Tue May 16 15:15:56 2023 +0200
+++ b/src/Pure/Isar/bundle.ML	Tue May 16 17:08:31 2023 +0200
@@ -59,13 +59,6 @@
 
 fun extern ctxt = Name_Space.extern ctxt (Name_Space.space_of_table (get_all ctxt));
 
-fun define_bundle (b, bundle) context =
-  let
-    val bundle' = Attrib.trim_context_thms bundle;
-    val (name, bundles') = Name_Space.define context true (b, bundle') (get_all_generic context);
-    val context' = (Data.map o apfst o K) bundles' context;
-  in (name, context') end;
-
 
 (* target -- bundle under construction *)
 
@@ -102,9 +95,24 @@
 
 (** define bundle **)
 
+(* context and morphisms *)
+
+val trim_context_bundle =
+  map (fn (fact, atts) => (map Thm.trim_context fact, (map o map) Token.trim_context atts));
+
+fun transfer_bundle thy =
+  map (fn (fact, atts) => (map (Thm.transfer thy) fact, (map o map) (Token.transfer thy) atts));
+
 fun transform_bundle phi =
   map (fn (fact, atts) => (Morphism.fact phi fact, (map o map) (Token.transform phi) atts));
 
+fun define_bundle (b, bundle) context =
+  let
+    val (name, bundles') = get_all_generic context
+      |> Name_Space.define context true (b, trim_context_bundle bundle);
+    val context' = (Data.map o apfst o K) bundles' context;
+  in (name, context') end;
+
 
 (* command *)
 
@@ -200,10 +208,13 @@
 local
 
 fun gen_activate notes prep_bundle args ctxt =
-  let val decls = maps (prep_bundle ctxt) args in
+  let
+    val thy = Proof_Context.theory_of ctxt;
+    val decls = maps (prep_bundle ctxt) args |> transfer_bundle thy;
+  in
     ctxt
     |> Context_Position.set_visible false
-    |> notes [(Binding.empty_atts, transform_bundle (Morphism.transfer_morphism' ctxt) decls)] |> #2
+    |> notes [(Binding.empty_atts, decls)] |> #2
     |> Context_Position.restore_visible ctxt
   end;
 
diff -r 7c9f290dff55 -r 4e865c45458b src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Tue May 16 15:15:56 2023 +0200
+++ b/src/Pure/Isar/class.ML	Tue May 16 17:08:31 2023 +0200
@@ -220,8 +220,11 @@
       (c, (class, ((ty, Free v_ty), false)))) params;
     val add_class = Graph.new_node (class,
         make_class_data (((map o apply2) fst params, base_sort,
-          base_morph, export_morph, Option.map Thm.trim_context some_assm_intro,
-          Thm.trim_context of_class, Option.map Thm.trim_context some_axiom),
+          Morphism.reset_context base_morph,
+          Morphism.reset_context export_morph,
+          Option.map Thm.trim_context some_assm_intro,
+          Thm.trim_context of_class,
+          Option.map Thm.trim_context some_axiom),
           (Thm.item_net, operations)))
       #> fold (curry Graph.add_edge class) sups;
   in Class_Data.map add_class thy end;
diff -r 7c9f290dff55 -r 4e865c45458b src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Tue May 16 15:15:56 2023 +0200
+++ b/src/Pure/Isar/element.ML	Tue May 16 17:08:31 2023 +0200
@@ -29,6 +29,8 @@
     ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
   val map_ctxt_attrib: (Token.src -> Token.src) ->
     ('typ, 'term, 'fact) ctxt -> ('typ, 'term, 'fact) ctxt
+  val trim_context_ctxt: context_i -> context_i
+  val transfer_ctxt: theory -> context_i -> context_i
   val transform_ctxt: morphism -> context_i -> context_i
   val pretty_stmt: Proof.context -> statement_i -> Pretty.T list
   val pretty_ctxt: Proof.context -> context_i -> Pretty.T list
@@ -103,6 +105,16 @@
 fun map_ctxt_attrib attrib =
   map_ctxt {binding = I, typ = I, term = I, pattern = I, fact = I, attrib = attrib};
 
+val trim_context_ctxt: context_i -> context_i = map_ctxt
+ {binding = I, typ = I, term = I, pattern = I,
+  fact = map Thm.trim_context,
+  attrib = map Token.trim_context};
+
+fun transfer_ctxt thy: context_i -> context_i = map_ctxt
+ {binding = I, typ = I, term = I, pattern = I,
+  fact = map (Thm.transfer thy),
+  attrib = map (Token.transfer thy)};
+
 fun transform_ctxt phi = map_ctxt
  {binding = Morphism.binding phi,
   typ = Morphism.typ phi,
diff -r 7c9f290dff55 -r 4e865c45458b src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Tue May 16 15:15:56 2023 +0200
+++ b/src/Pure/Isar/expression.ML	Tue May 16 17:08:31 2023 +0200
@@ -851,7 +851,7 @@
 
     val notes' =
       body_elems
-      |> map (Element.transform_ctxt (Morphism.transfer_morphism thy'))
+      |> map (Element.transfer_ctxt thy')
       |> map (defines_to_notes pred_ctxt)
       |> map (Element.transform_ctxt a_satisfy)
       |> (fn elems =>
diff -r 7c9f290dff55 -r 4e865c45458b src/Pure/Isar/interpretation.ML
--- a/src/Pure/Isar/interpretation.ML	Tue May 16 15:15:56 2023 +0200
+++ b/src/Pure/Isar/interpretation.ML	Tue May 16 17:08:31 2023 +0200
@@ -104,9 +104,7 @@
       fold_map (fn facts => note Thm.theoremK facts #-> abs_def_rule) factss ctxt;
     val defs = (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]);
     val (eqns', ctxt'') = ctxt' |> note Thm.theoremK [defs] |-> abs_def_rule;
-    val transform_witness =
-      Element.transform_witness
-        (Morphism.transfer_morphism' ctxt' $> export' $> Morphism.trim_context_morphism);
+    val transform_witness = Element.transform_witness (Morphism.set_trim_context' ctxt' export');
     val deps' =
       (deps ~~ witss) |> map (fn ((dep, morph), wits) =>
         (dep, morph $> Element.satisfy_morphism (map transform_witness wits)));
diff -r 7c9f290dff55 -r 4e865c45458b src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Tue May 16 15:15:56 2023 +0200
+++ b/src/Pure/Isar/local_theory.ML	Tue May 16 17:08:31 2023 +0200
@@ -192,9 +192,10 @@
 (* standard morphisms *)
 
 fun standard_morphism lthy ctxt =
-  Proof_Context.norm_export_morphism lthy ctxt $>
-  Morphism.binding_morphism "Local_Theory.standard_binding"
-    (Name_Space.transform_binding (Proof_Context.naming_of lthy));
+  Morphism.set_context' lthy
+   (Proof_Context.norm_export_morphism lthy ctxt $>
+    Morphism.binding_morphism "Local_Theory.standard_binding"
+      (Name_Space.transform_binding (Proof_Context.naming_of lthy)));
 
 fun standard_morphism_theory lthy =
   standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy));
diff -r 7c9f290dff55 -r 4e865c45458b src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue May 16 15:15:56 2023 +0200
+++ b/src/Pure/Isar/locale.ML	Tue May 16 17:08:31 2023 +0200
@@ -213,10 +213,11 @@
     (binding,
       mk_locale ((parameters, spec, (apply2 o Option.map) Thm.trim_context intros,
           map Thm.trim_context axioms,
-          map (Element.transform_ctxt Morphism.trim_context_morphism) hyp_spec),
+          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, (morph, Morphism.identity))) dependencies,
+          (map (fn (name, morph) =>
+                make_dep (name, (Morphism.reset_context morph, Morphism.identity))) dependencies,
             Inttab.empty)))) #> snd);
           (* FIXME Morphism.identity *)
 
@@ -650,7 +651,7 @@
       val applied_notes = make_notes kind facts;
 
       fun apply_notes morph = applied_notes |> fold (fn elem => fn context =>
-        let val elem' = Element.transform_ctxt (Morphism.transfer_morphism'' context $> morph) elem
+        let val elem' = Element.transform_ctxt (Morphism.set_context'' context morph) elem
         in Element.init elem' context end);
       val apply_registrations = Context.theory_map (fn context =>
         fold_rev (apply_notes o #2) (registrations_of context loc) context);
diff -r 7c9f290dff55 -r 4e865c45458b src/Pure/Isar/spec_rules.ML
--- a/src/Pure/Isar/spec_rules.ML	Tue May 16 15:15:56 2023 +0200
+++ b/src/Pure/Isar/spec_rules.ML	Tue May 16 17:08:31 2023 +0200
@@ -162,14 +162,13 @@
     lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
       (fn phi => fn context =>
         let
+          val psi = Morphism.set_trim_context'' context phi;
           val pos = Position.thread_data ();
-          val name = Name_Space.full_name (Name_Space.naming_of context) (Morphism.binding phi b);
+          val name = Name_Space.full_name (Name_Space.naming_of context) (Morphism.binding psi b);
           val (terms', rules') =
-            map (Thm.transfer (Context.theory_of context)) thms0
-            |> Morphism.fact phi
+            Morphism.fact psi thms0
             |> chop (length terms)
-            |>> map (Thm.term_of o Drule.dest_term)
-            ||> map Thm.trim_context;
+            |>> map (Thm.term_of o Drule.dest_term);
         in
           context |> (Data.map o Item_Net.update)
             {pos = pos, name = name, rough_classification = rough_classification,
diff -r 7c9f290dff55 -r 4e865c45458b src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Tue May 16 15:15:56 2023 +0200
+++ b/src/Pure/Isar/token.ML	Tue May 16 17:08:31 2023 +0200
@@ -82,7 +82,8 @@
   val get_name: T -> name_value option
   val declare_maxidx: T -> Proof.context -> Proof.context
   val map_facts: (string option -> thm list -> thm list) -> T -> T
-  val trim_context_src: src -> src
+  val trim_context: T -> T
+  val transfer: theory -> T -> T
   val transform: morphism -> T -> T
   val init_assignable: T -> T
   val assign: value option -> T -> T
@@ -484,7 +485,26 @@
     | Fact (a, ths) => Fact (a, f a ths)
     | _ => v));
 
-val trim_context_src = (map o map_facts) (K (map Thm.trim_context));
+
+(* implicit context *)
+
+local
+
+fun context thm_context morphism_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)
+        | 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);
+
+end;
 
 
 (* transform *)
diff -r 7c9f290dff55 -r 4e865c45458b src/Pure/ex/Def.thy
--- a/src/Pure/ex/Def.thy	Tue May 16 15:15:56 2023 +0200
+++ b/src/Pure/ex/Def.thy	Tue May 16 17:08:31 2023 +0200
@@ -46,7 +46,7 @@
   in
     lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
       (fn phi => fn context =>
-        let val psi = Morphism.transfer_morphism'' context $> phi $> Morphism.trim_context_morphism
+        let val psi = Morphism.set_trim_context'' context phi
         in (Data.map o Item_Net.update) (transform_def psi def) context end)
   end;
 
diff -r 7c9f290dff55 -r 4e865c45458b src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Tue May 16 15:15:56 2023 +0200
+++ b/src/Pure/morphism.ML	Tue May 16 17:08:31 2023 +0200
@@ -53,6 +53,9 @@
   val transfer_morphism': Proof.context -> morphism
   val transfer_morphism'': Context.generic -> morphism
   val trim_context_morphism: morphism
+  val set_trim_context: theory -> morphism -> morphism
+  val set_trim_context': Proof.context -> morphism -> morphism
+  val set_trim_context'': Context.generic -> morphism -> morphism
   val instantiate_frees_morphism: ctyp TFrees.table * cterm Frees.table -> morphism
   val instantiate_morphism: ctyp TVars.table * cterm Vars.table -> morphism
 end;
@@ -183,6 +186,10 @@
 
 val trim_context_morphism = thm_morphism "trim_context" Thm.trim_context;
 
+fun set_trim_context thy phi = set_context thy phi $> trim_context_morphism;
+val set_trim_context' = set_trim_context o Proof_Context.theory_of;
+val set_trim_context'' = set_trim_context o Context.theory_of;
+
 
 (* instantiate *)