src/Pure/ML/ml_thms.ML

--- a/src/Pure/ML/ml_thms.ML	Fri Feb 23 21:12:08 2018 +0100
+++ b/src/Pure/ML/ml_thms.ML	Fri Feb 23 21:27:20 2018 +0100
@@ -120,8 +120,9 @@
 
 fun ml_store get (name, ths) =
   let
-    val ths' = Context.>>> (Context.map_theory_result
-      (Global_Theory.store_thms (Binding.name name, ths)));
+    val (_, ths') =
+      Context.>>> (Context.map_theory_result
+        (Global_Theory.note_thms "" ((Binding.name name, []), [(ths, [])])));
     val _ = Theory.setup (Stored_Thms.put ths');
     val _ =
       if name = "" then ()