src/Pure/ML/ml_thms.ML

       in thm_binding "lemma" (length (flat propss) = 1) thms ctxt end));
 
 
 (* old-style theorem bindings *)
 
-structure Stored_Thms = Theory_Data
+structure Data = Theory_Data
 (
   type T = thm list;
   val empty = [];
-  fun extend _ = [];
-  fun merge _ = [];
+  val extend = I;
+  val merge = #1;
 );
 
-fun get_stored_thms () = Stored_Thms.get (Context.the_global_context ());
+fun get_stored_thms () = Data.get (Context.the_global_context ());
 val get_stored_thm = hd o get_stored_thms;
 
 fun ml_store get (name, ths) =
   let
     val (_, ths') =
       Context.>>> (Context.map_theory_result
         (Global_Theory.note_thms "" ((Binding.name name, []), [(ths, [])])));
-    val _ = Theory.setup (Stored_Thms.put ths');
+    val _ = Theory.setup (Data.put ths');
     val _ =
       if name = "" then ()
       else if not (ML_Syntax.is_identifier name) then
         error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value")
       else
         ML_Compiler.eval (ML_Compiler.verbose true ML_Compiler.flags) Position.none
           (ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();"));
-    val _ = Theory.setup (Stored_Thms.put []);
+    val _ = Theory.setup (Data.put []);
   in () end;
 
 val store_thms = ml_store "ML_Thms.get_stored_thms";
 fun store_thm (name, th) = ml_store "ML_Thms.get_stored_thm" (name, [th]);