src/Pure/ML/ml_context.ML

--- a/src/Pure/ML/ml_context.ML	Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/ML/ml_context.ML	Mon Sep 20 16:05:25 2010 +0200
@@ -75,7 +75,7 @@
 fun ml_store get (name, ths) =
   let
     val ths' = Context.>>> (Context.map_theory_result
-      (PureThy.store_thms (Binding.name name, ths)));
+      (Global_Theory.store_thms (Binding.name name, ths)));
     val _ = Context.>> (Context.map_theory (Stored_Thms.put ths'));
     val _ =
       if name = "" then ()