diff -r 54cebc5cd108 -r 1004333b76aa src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Tue Aug 06 16:13:59 2019 +0200
+++ b/src/Pure/Isar/object_logic.ML	Tue Aug 06 16:15:22 2019 +0200
@@ -171,8 +171,9 @@
 
 (* maintain rules *)
 
-val get_atomize = #1 o #atomize_rulify o get_data;
-val get_rulify = #2 o #atomize_rulify o get_data;
+fun get_atomize_rulify f ctxt = map (Thm.transfer' ctxt) (f (#atomize_rulify (get_data ctxt)));
+val get_atomize = get_atomize_rulify #1;
+val get_rulify = get_atomize_rulify #2;
 
 fun add_atomize th = map_data (fn (base_sort, judgment, (atomize, rulify)) =>
   (base_sort, judgment, (Thm.add_thm (Thm.trim_context th) atomize, rulify)));