# HG changeset patch
# User wenzelm
# Date 896124304 -7200
# Node ID bbe9065edf8ac3de3b67bf69718dd1465e2eb80d
# Parent  38aa2d56e28cdfbb2d5df84a0299f6eeccea2526
tuned store_theory: theory -> unit;

diff -r 38aa2d56e28c -r bbe9065edf8a src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Mon May 25 21:24:27 1998 +0200
+++ b/src/Pure/Thy/thy_info.ML	Mon May 25 21:25:04 1998 +0200
@@ -32,7 +32,7 @@
 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
@@ -111,8 +111,9 @@
 
 (* 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,