tuned store_theory: theory -> unit;
authorwenzelm
Mon, 25 May 1998 21:25:04 +0200
changeset 4964 bbe9065edf8a
parent 4963 38aa2d56e28c
child 4965 06914837e073
tuned store_theory: theory -> unit;
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,