add_thydata and get_thydata now take a string as their first argument

--- a/src/Pure/Thy/thy_read.ML	Fri Apr 12 12:41:26 1996 +0200
+++ b/src/Pure/Thy/thy_read.ML	Fri Apr 12 12:41:59 1996 +0200
@@ -84,8 +84,8 @@
   val thms_of        : theory -> (string * thm) list
   val delete_thms    : string -> unit
 
-  val add_thydata    : theory -> string * thy_methods -> unit
-  val get_thydata    : theory -> string -> exn option
+  val add_thydata    : string -> string * thy_methods -> unit
+  val get_thydata    : string -> string -> exn option
   val add_thy_reader_file: string -> unit
   val set_thy_reader_file: string -> unit
   val read_thy_reader_files: unit -> unit
@@ -1315,10 +1315,12 @@
 (*** Misc functions ***)
 
 (*Add data handling methods to theory*)
-fun add_thydata thy (new_methods as (id, ThyMethods {get, ...})) =
-  let val (tname, ThyInfo {path, children, parents, thy_time, ml_time, theory,
-                           thms, methods, data}) =
-        thyinfo_of_sign (sign_of thy);
+fun add_thydata tname (new_methods as (id, ThyMethods {get, ...})) =
+  let val ThyInfo {path, children, parents, thy_time, ml_time, theory,
+                   thms, methods, data} =
+        case get_thyinfo tname of
+            Some ti => ti
+          | None => error ("Theory " ^ tname ^ " not stored by loader");
   in loaded_thys := Symtab.update ((tname, ThyInfo {path = path,
        children = children, parents = parents, thy_time = thy_time,
        ml_time = ml_time, theory = theory, thms = thms,
@@ -1339,9 +1341,10 @@
 
 
 (*Retrieve data associated with theory*)
-fun get_thydata thy id =
-  let val (tname, ThyInfo {data = (_, d2), ...}) =
-        thyinfo_of_sign (sign_of thy);
+fun get_thydata tname id =
+  let val d2 = case get_thyinfo tname of
+                   Some (ThyInfo {data, ...}) => snd data
+                 | None => error ("Theory " ^ tname ^ " not stored by loader");
   in Symtab.lookup (d2, id) end;