src/Pure/drule.ML

--- a/src/Pure/drule.ML	Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/drule.ML	Mon Sep 20 16:05:25 2010 +0200
@@ -433,10 +433,10 @@
 val read_prop = certify o Simple_Syntax.read_prop;
 
 fun store_thm name th =
-  Context.>>> (Context.map_theory_result (PureThy.store_thm (name, th)));
+  Context.>>> (Context.map_theory_result (Global_Theory.store_thm (name, th)));
 
 fun store_thm_open name th =
-  Context.>>> (Context.map_theory_result (PureThy.store_thm_open (name, th)));
+  Context.>>> (Context.map_theory_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 thm = store_thm_open name (export_without_context_open thm);