# HG changeset patch
# User wenzelm
# Date 1682083571 -7200
# Node ID 42214742b44a8b915c47e0e158c072d297133e8a
# Parent  c6fcf32010d1505bedb9408d335ae8198bf13615
proper Thm.trim_context / Thm.transfer for context data;

diff -r c6fcf32010d1 -r 42214742b44a src/HOL/Analysis/measurable.ML
--- a/src/HOL/Analysis/measurable.ML	Fri Apr 21 15:14:14 2023 +0200
+++ b/src/HOL/Analysis/measurable.ML	Fri Apr 21 15:26:11 2023 +0200
@@ -75,7 +75,7 @@
 fun generic_add_del map : attribute context_parser =
   Scan.lift
     (Args.add >> K Item_Net.update || Args.del >> K Item_Net.remove || Scan.succeed Item_Net.update) >>
-    (fn f => Thm.declaration_attribute (map o f))
+    (fn f => Thm.declaration_attribute (map o f o Thm.trim_context))
 
 val dest_thm_attr = generic_add_del map_dest_thms
 val cong_thm_attr = generic_add_del map_cong_thms
@@ -86,13 +86,13 @@
   in fold Item_Net.remove thms net end ;
 
 fun measurable_thm_attr (do_add, d) = Thm.declaration_attribute
-  (map_measurable_thms o (if do_add then Item_Net.update o rpair d else del_thm))
-
-val get_dest = Item_Net.content o #2 o Data.get;
+  (map_measurable_thms o (if do_add then Item_Net.update o rpair d else del_thm) o Thm.trim_context)
 
-val get_cong = Item_Net.content o #3 o Data.get;
-val add_cong = map_cong_thms o Item_Net.update;
-val del_cong = map_cong_thms o Item_Net.remove;
+fun get_dest context = map (Thm.transfer'' context) (Item_Net.content (#2 (Data.get context)));
+fun get_cong context = map (Thm.transfer'' context) (Item_Net.content (#3 (Data.get context)));
+
+val add_cong = map_cong_thms o Item_Net.update o Thm.trim_context;
+val del_cong = map_cong_thms o Item_Net.remove o Thm.trim_context;
 fun add_del_cong_thm true = add_cong
   | add_del_cong_thm false = del_cong
 
@@ -108,9 +108,10 @@
     val concl' = HOLogic.dest_Trueprop concl handle TERM _ => concl
   in is_Var (head_of concl') end
 
-val get_thms = Data.get #> #1 #> Item_Net.content ;
+fun get_thms context =
+  map (apfst (Thm.transfer'' context)) (Item_Net.content (#1 (Data.get context)));
 
-val get_all = get_thms #> map fst ;
+val get_all = get_thms #> map fst;
 
 fun debug_tac ctxt msg f =
   if Config.get ctxt debug then print_tac ctxt (msg ()) THEN f else f