src/Pure/drule.ML
changeset 78795 f7e972d567f3
parent 78136 e1bd2eb4c407
child 79412 1c758cd8d5b2
--- 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);