--- a/src/Pure/drule.ML Tue Oct 17 22:29:12 2023 +0200
+++ b/src/Pure/drule.ML Wed Oct 18 15:13:52 2023 +0200
@@ -337,10 +337,10 @@
val read_prop = certify o Simple_Syntax.read_prop;
fun store_thm name th =
- Context.>>> (Context.map_theory_result (Global_Theory.store_thm (name, th)));
+ Theory.setup_result (Global_Theory.store_thm (name, th));
fun store_thm_open name th =
- Context.>>> (Context.map_theory_result (Global_Theory.store_thm_open (name, th)));
+ Theory.setup_result (Global_Theory.store_thm_open (name, th));
fun store_standard_thm name th = store_thm name (export_without_context th);
fun store_standard_thm_open name th = store_thm_open name (export_without_context_open th);