src/Pure/Thy/thy_info.ML

 
 signature THY_INFO =
 sig
   val loaded_thys: thy_info Symtab.table ref
   val get_thyinfo: string -> thy_info option
-  val store_theory: theory * string -> unit
+  val store_theory: theory -> unit
   val path_of: string -> string
   val children_of: string -> string list
   val parents_of_name: string -> string list
   val thyinfo_of_sign: Sign.sg -> string * thy_info
   val theory_of: string -> theory

   | _ => err_not_stored name);
 
 
 (* store_theory *)
 
-fun store_theory (thy, name) =
+fun store_theory thy =
   let
+    val name = PureThy.get_name thy;
     val {path, children, parents, thy_time, ml_time, theory = _} =
       the_thyinfo name;
     val info = {path = path, children = children, parents = parents,
       thy_time = thy_time, ml_time = ml_time, theory = Some thy};
   in