# HG changeset patch
# User wenzelm
# Date 1519417640 -3600
# Node ID ec46ecb879999a37c46194e0a3e4eeb55353b7cc
# Parent  a0b58be402abaa98b008daf98e202262a897feab
tuned signature;

diff -r a0b58be402ab -r ec46ecb87999 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 ()
diff -r a0b58be402ab -r ec46ecb87999 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Fri Feb 23 21:12:08 2018 +0100
+++ b/src/Pure/global_theory.ML	Fri Feb 23 21:27:20 2018 +0100
@@ -25,7 +25,6 @@
   val name_thms: bool -> bool -> string -> thm list -> thm list
   val name_thmss: bool -> string -> (thm list * 'a) list -> (thm list * 'a) list
   val add_thms_lazy: string -> (binding * thm list lazy) -> theory -> theory
-  val store_thms: binding * thm list -> theory -> thm list * theory
   val store_thm: binding * thm -> theory -> thm * theory
   val store_thm_open: binding * thm -> theory -> thm * theory
   val add_thms: ((binding * thm) * attribute list) list -> theory -> thm list * theory
@@ -151,12 +150,10 @@
     in (map (Thm.transfer thy'') thms', thy'') end;
 
 
-(* store_thm(s) *)
+(* store_thm *)
 
-fun store_thms (b, thms) =
-  enter_thms (name_thms true true) (name_thms false true) pair (b, thms);
-
-fun store_thm (b, th) = store_thms (b, [th]) #>> the_single;
+fun store_thm (b, th) =
+  enter_thms (name_thms true true) (name_thms false true) pair (b, [th]) #>> the_single;
 
 fun store_thm_open (b, th) =
   enter_thms (name_thms true false) (name_thms false false) pair (b, [th]) #>> the_single;