clarified signature;
more careful treatment of implicit context;

--- a/src/HOL/Tools/Lifting/lifting_def.ML	Tue Aug 06 16:29:28 2019 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Tue Aug 06 17:26:40 2019 +0200
@@ -624,7 +624,7 @@
   let
     fun collect (data : Lifting_Info.quotient) l =
       if is_some (#pcr_info data)
-      then ((Thm.symmetric o safe_mk_meta_eq o #pcr_cr_eq o the o #pcr_info) data :: l)
+      then ((Thm.symmetric o safe_mk_meta_eq o Thm.transfer' ctxt o #pcr_cr_eq o the o #pcr_info) data :: l)
       else l
     val table = Lifting_Info.get_quotients ctxt
   in

--- a/src/HOL/Tools/Lifting/lifting_info.ML	Tue Aug 06 16:29:28 2019 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML	Tue Aug 06 17:26:40 2019 +0200
@@ -185,7 +185,7 @@
     val rel_quot_thm_concl = (Logic.strip_imp_concl o Thm.prop_of) rel_quot_thm
     val (_, abs, _, _) = (dest_Quotient o HOLogic.dest_Trueprop) rel_quot_thm_concl
     val relatorT_name = (fst o dest_Type o fst o dest_funT o fastype_of) abs
-    val minfo = {rel_quot_thm = rel_quot_thm}
+    val minfo = {rel_quot_thm = Thm.trim_context rel_quot_thm}
   in
     Data.map (map_quot_maps (Symtab.update (relatorT_name, minfo))) context
   end
@@ -218,7 +218,9 @@
 fun transform_quotient phi {quot_thm, pcr_info} =
   {quot_thm = Morphism.thm phi quot_thm, pcr_info = Option.map (transform_pcr_info phi) pcr_info}
 
-fun lookup_quotients ctxt type_name = Symtab.lookup (get_quotients ctxt) type_name
+fun lookup_quotients ctxt type_name =
+  Symtab.lookup (get_quotients ctxt) type_name
+  |> Option.map (transform_quotient (Morphism.transfer_morphism' ctxt))
 
 fun lookup_quot_thm_quotients ctxt quot_thm =
   let
@@ -232,7 +234,8 @@
   end
 
 fun update_quotients type_name qinfo context =
-  Data.map (map_quotients (Symtab.update (type_name, qinfo))) context
+  let val qinfo' = transform_quotient Morphism.trim_context_morphism qinfo
+  in Data.map (map_quotients (Symtab.update (type_name, qinfo'))) context end
 
 fun delete_quotients quot_thm context =
   let
@@ -292,9 +295,13 @@
 
 (* info about reflexivity rules *)
 
-val get_reflexivity_rules = Item_Net.content o get_reflexivity_rules' o Context.Proof
+fun get_reflexivity_rules ctxt =
+  Item_Net.content (get_reflexivity_rules' (Context.Proof ctxt))
+  |> map (Thm.transfer' ctxt)
 
-fun add_reflexivity_rule thm = Data.map (map_reflexivity_rules (Item_Net.update thm))
+fun add_reflexivity_rule thm =
+  Data.map (map_reflexivity_rules (Item_Net.update (Thm.trim_context thm)))
+
 val add_reflexivity_rule_attribute = Thm.declaration_attribute add_reflexivity_rule
 
 
@@ -360,16 +367,19 @@
 
 fun add_reflexivity_rules mono_rule context =
   let
-    fun find_eq_rule thm ctxt =
+    val ctxt = Context.proof_of context
+    val thy = Context.theory_of context
+
+    fun find_eq_rule thm =
       let
-        val concl_rhs = (hd o get_args 1 o HOLogic.dest_Trueprop o Thm.concl_of) thm;
-        val rules = Item_Net.retrieve (Transfer.get_relator_eq_item_net ctxt) concl_rhs;
+        val concl_rhs = (hd o get_args 1 o HOLogic.dest_Trueprop o Thm.concl_of) thm
+        val rules = Transfer.retrieve_relator_eq ctxt concl_rhs
       in
-        find_first (fn thm => Pattern.matches (Proof_Context.theory_of ctxt) (concl_rhs,
-          (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.concl_of) thm)) rules
+        find_first (fn th => Pattern.matches thy (concl_rhs,
+          (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.concl_of) th)) rules
       end
 
-    val eq_rule = find_eq_rule mono_rule (Context.proof_of context);
+    val eq_rule = find_eq_rule mono_rule;
     val eq_rule = if is_some eq_rule then the eq_rule else error
       "No corresponding rule that the relator preserves equality was found."
   in
@@ -505,13 +515,17 @@
     end
 end
 
-fun get_distr_rules_raw context = Symtab.fold
-  (fn (_, {pos_distr_rules, neg_distr_rules, ...}) => fn rules => pos_distr_rules @ neg_distr_rules @ rules)
+fun get_distr_rules_raw context =
+  Symtab.fold (fn (_, {pos_distr_rules, neg_distr_rules, ...}) => fn rules =>
+      pos_distr_rules @ neg_distr_rules @ rules)
     (get_relator_distr_data' context) []
+  |> map (Thm.transfer'' context)
 
-fun get_mono_rules_raw context = Symtab.fold
-  (fn (_, {pos_mono_rule, neg_mono_rule, ...}) => fn rules => [pos_mono_rule, neg_mono_rule] @ rules)
+fun get_mono_rules_raw context =
+  Symtab.fold (fn (_, {pos_mono_rule, neg_mono_rule, ...}) => fn rules =>
+      [pos_mono_rule, neg_mono_rule] @ rules)
     (get_relator_distr_data' context) []
+  |> map (Thm.transfer'' context)
 
 val lookup_relator_distr_data = Symtab.lookup o get_relator_distr_data
 

--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Tue Aug 06 16:29:28 2019 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Tue Aug 06 17:26:40 2019 +0200
@@ -426,10 +426,10 @@
         thm |> Thm.cprop_of |> Drule.strip_imp_concl
         |> Thm.dest_arg |> Thm.dest_arg1 |> Thm.dest_arg
       val pcrel_def = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) pcrel_def
-      val thm = Thm.instantiate (Thm.match (ct, Thm.rhs_of pcrel_def)) thm
+      val thm' = Thm.instantiate (Thm.match (ct, Thm.rhs_of pcrel_def)) thm
         handle Pattern.MATCH => raise CTERM ("fold_Domainp_pcrel", [ct, Thm.rhs_of pcrel_def])
     in
-      rewrite_first_Domainp_arg (Thm.symmetric pcrel_def) thm
+      rewrite_first_Domainp_arg (Thm.symmetric pcrel_def) thm'
     end
 
   fun reduce_Domainp ctxt rules thm =

--- a/src/HOL/Tools/Transfer/transfer.ML	Tue Aug 06 16:29:28 2019 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML	Tue Aug 06 17:26:40 2019 +0200
@@ -22,16 +22,16 @@
   val fold_relator_eqs_conv: Proof.context -> conv
   val unfold_relator_eqs_conv: Proof.context -> conv
   val get_transfer_raw: Proof.context -> thm list
-  val get_relator_eq_item_net: Proof.context -> thm Item_Net.T
   val get_relator_eq: Proof.context -> thm list
+  val retrieve_relator_eq: Proof.context -> term -> thm list
   val get_sym_relator_eq: Proof.context -> thm list
   val get_relator_eq_raw: Proof.context -> thm list
   val get_relator_domain: Proof.context -> thm list
   val morph_pred_data: morphism -> pred_data -> pred_data
   val lookup_pred_data: Proof.context -> string -> pred_data option
   val update_pred_data: string -> pred_data -> Context.generic -> Context.generic
-  val get_compound_lhs: Proof.context -> (term * thm) Item_Net.T
-  val get_compound_rhs: Proof.context -> (term * thm) Item_Net.T
+  val is_compound_lhs: Proof.context -> term -> bool
+  val is_compound_rhs: Proof.context -> term -> bool
   val transfer_add: attribute
   val transfer_del: attribute
   val transfer_raw_add: thm -> Context.generic -> Context.generic
@@ -67,7 +67,7 @@
 val rewr_rules = Item_Net.init Thm.eq_thm_prop (single o fst o HOLogic.dest_eq
   o HOLogic.dest_Trueprop o Thm.concl_of);
 
-datatype pred_data = PRED_DATA of {pred_def:thm, rel_eq_onp: thm, pred_simps: thm list}
+datatype pred_data = PRED_DATA of {pred_def: thm, rel_eq_onp: thm, pred_simps: thm list}
 
 fun mk_pred_data pred_def rel_eq_onp pred_simps = PRED_DATA {pred_def = pred_def, 
   rel_eq_onp = rel_eq_onp, pred_simps = pred_simps}
@@ -124,25 +124,32 @@
       pred_data = Symtab.merge (K true) (pd1, pd2) }
 )
 
-val get_transfer_raw = Item_Net.content o #transfer_raw o Data.get o Context.Proof
+fun get_net_content f ctxt =
+  Item_Net.content (f (Data.get (Context.Proof ctxt)))
+  |> map (Thm.transfer' ctxt)
+
+val get_transfer_raw = get_net_content #transfer_raw
 
 val get_known_frees = #known_frees o Data.get o Context.Proof
 
-val get_compound_lhs = #compound_lhs o Data.get o Context.Proof
+fun is_compound f ctxt t =
+  Item_Net.retrieve (f (Data.get (Context.Proof ctxt))) t
+  |> exists (fn (pat, _) => Pattern.matches (Proof_Context.theory_of ctxt) (pat, t));
 
-val get_compound_rhs = #compound_rhs o Data.get o Context.Proof
+val is_compound_lhs = is_compound #compound_lhs
+val is_compound_rhs = is_compound #compound_rhs
 
-val get_relator_eq_item_net = #relator_eq o Data.get o Context.Proof
+val get_relator_eq = get_net_content #relator_eq #> map safe_mk_meta_eq
 
-val get_relator_eq =
-  map safe_mk_meta_eq o Item_Net.content o #relator_eq o Data.get o Context.Proof
+fun retrieve_relator_eq ctxt t =
+  Item_Net.retrieve (#relator_eq (Data.get (Context.Proof ctxt))) t
+  |> map (Thm.transfer' ctxt)
 
-val get_sym_relator_eq =
-  map (Thm.symmetric o safe_mk_meta_eq) o Item_Net.content o #relator_eq o Data.get o Context.Proof
+val get_sym_relator_eq = get_net_content #relator_eq #> map (safe_mk_meta_eq #> Thm.symmetric)
 
-val get_relator_eq_raw = Item_Net.content o #relator_eq_raw o Data.get o Context.Proof
+val get_relator_eq_raw = get_net_content #relator_eq_raw
 
-val get_relator_domain = Item_Net.content o #relator_domain o Data.get o Context.Proof
+val get_relator_domain = get_net_content #relator_domain
 
 val get_pred_data = #pred_data o Data.get o Context.Proof
 
@@ -167,19 +174,20 @@
 fun map_relator_domain f = map_data I I I I I I f I
 fun map_pred_data      f = map_data I I I I I I I f
 
-fun add_transfer_thm thm = Data.map
-  (map_transfer_raw (Item_Net.update thm) o
-   map_compound_lhs
-     (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
-        Const (\<^const_name>\<open>Rel\<close>, _) $ _ $ (lhs as (_ $ _)) $ _ =>
-          Item_Net.update (lhs, thm)
-      | _ => I) o
-   map_compound_rhs
-     (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
-        Const (\<^const_name>\<open>Rel\<close>, _) $ _ $ _ $ (rhs as (_ $ _)) =>
-          Item_Net.update (rhs, thm)
-      | _ => I) o
-   map_known_frees (Term.add_frees (Thm.concl_of thm)))
+val add_transfer_thm =
+  Thm.trim_context #> (fn thm => Data.map
+    (map_transfer_raw (Item_Net.update thm) o
+     map_compound_lhs
+       (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
+          Const (\<^const_name>\<open>Rel\<close>, _) $ _ $ (lhs as (_ $ _)) $ _ =>
+            Item_Net.update (lhs, thm)
+        | _ => I) o
+     map_compound_rhs
+       (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
+          Const (\<^const_name>\<open>Rel\<close>, _) $ _ $ _ $ (rhs as (_ $ _)) =>
+            Item_Net.update (rhs, thm)
+        | _ => I) o
+     map_known_frees (Term.add_frees (Thm.concl_of thm))))
 
 fun del_transfer_thm thm = Data.map
   (map_transfer_raw (Item_Net.remove thm) o
@@ -560,16 +568,9 @@
     map_filter f (Symtab.dest tab)
   end
 
-fun retrieve_terms t net = map fst (Item_Net.retrieve net t)
-
-fun matches_list ctxt term =
-  is_some o find_first (fn pat => Pattern.matches (Proof_Context.theory_of ctxt) (pat, term))
-
 fun transfer_rule_of_term ctxt equiv t =
   let
-    val compound_rhs = get_compound_rhs ctxt
-    fun is_rhs t = compound_rhs |> retrieve_terms t |> matches_list ctxt t
-    val s = skeleton is_rhs ctxt t
+    val s = skeleton (is_compound_rhs ctxt) ctxt t
     val frees = map fst (Term.add_frees s [])
     val tfrees = map fst (Term.add_tfrees s [])
     fun prep a = "R" ^ Library.unprefix "'" a
@@ -590,9 +591,7 @@
 
 fun transfer_rule_of_lhs ctxt t =
   let
-    val compound_lhs = get_compound_lhs ctxt
-    fun is_lhs t = compound_lhs |> retrieve_terms t |> matches_list ctxt t
-    val s = skeleton is_lhs ctxt t
+    val s = skeleton (is_compound_lhs ctxt) ctxt t
     val frees = map fst (Term.add_frees s [])
     val tfrees = map fst (Term.add_tfrees s [])
     fun prep a = "R" ^ Library.unprefix "'" a
@@ -853,10 +852,12 @@
   Theory.setup
     let
       val name = \<^binding>\<open>relator_eq\<close>
-      fun add_thm thm context = context
-        |> Data.map (map_relator_eq (Item_Net.update thm))
+      fun add_thm thm context =
+        context
+        |> Data.map (map_relator_eq (Item_Net.update (Thm.trim_context thm)))
         |> Data.map (map_relator_eq_raw
-            (Item_Net.update (abstract_equalities_relator_eq (Context.proof_of context) thm)))
+            (Item_Net.update
+              (Thm.trim_context (abstract_equalities_relator_eq (Context.proof_of context) thm))))
       fun del_thm thm context = context
         |> Data.map (map_relator_eq (Item_Net.remove thm))
         |> Data.map (map_relator_eq_raw
@@ -876,15 +877,21 @@
       val name = \<^binding>\<open>relator_domain\<close>
       fun add_thm thm context =
         let
-          val thm = abstract_domains_relator_domain (Context.proof_of context) thm
+          val thm' = thm
+            |> abstract_domains_relator_domain (Context.proof_of context)
+            |> Thm.trim_context
         in
-          context |> Data.map (map_relator_domain (Item_Net.update thm)) |> add_transfer_domain_thm thm
+          context
+          |> Data.map (map_relator_domain (Item_Net.update thm'))
+          |> add_transfer_domain_thm thm'
         end
       fun del_thm thm context =
         let
-          val thm = abstract_domains_relator_domain (Context.proof_of context) thm
+          val thm' = abstract_domains_relator_domain (Context.proof_of context) thm
         in
-          context |> Data.map (map_relator_domain (Item_Net.remove thm)) |> del_transfer_domain_thm thm
+          context
+          |> Data.map (map_relator_domain (Item_Net.remove thm'))
+          |> del_transfer_domain_thm thm'
         end
       val add = Thm.declaration_attribute add_thm
       val del = Thm.declaration_attribute del_thm