src/HOL/Tools/Transfer/transfer_bnf.ML

     val (pred_notes, lthy) = predicator bnf lthy
   in
     snd (Local_Theory.notes (constr_notes @ relator_eq_notes @ pred_notes) lthy)
   end
 
-val _ = Context.>> (Context.map_theory (bnf_interpretation
+val _ = Theory.setup (bnf_interpretation
   (bnf_only_type_ctr (map_local_theory o transfer_bnf_interpretation))
-  (bnf_only_type_ctr (transfer_bnf_interpretation))))
+  (bnf_only_type_ctr (transfer_bnf_interpretation)))
 
 (* simplification rules for the predicator *)
 
 fun lookup_defined_pred_data lthy name =
   case (Transfer.lookup_pred_data lthy name) of

     val simp_attrs = @{attributes [simp]}
   in
     snd (Local_Theory.note ((pred_inject_thm_name, simp_attrs), pred_injects) lthy)
   end
 
-val _ = Context.>> (Context.map_theory (fp_sugar_interpretation
+val _ = Theory.setup (fp_sugar_interpretation
   (fp_sugar_only_type_ctr (map_local_theory o fold transfer_fp_sugar_interpretation))
-  (fp_sugar_only_type_ctr (fold transfer_fp_sugar_interpretation))))
+  (fp_sugar_only_type_ctr (fold transfer_fp_sugar_interpretation)))
 
 end