src/Pure/Thy/thy_info.ML
changeset 4964 bbe9065edf8a
parent 4111 93baba60ece2
child 4975 20b89fcd90a7
     1.1 --- a/src/Pure/Thy/thy_info.ML	Mon May 25 21:24:27 1998 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Mon May 25 21:25:04 1998 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4  sig
     1.5    val loaded_thys: thy_info Symtab.table ref
     1.6    val get_thyinfo: string -> thy_info option
     1.7 -  val store_theory: theory * string -> unit
     1.8 +  val store_theory: theory -> unit
     1.9    val path_of: string -> string
    1.10    val children_of: string -> string list
    1.11    val parents_of_name: string -> string list
    1.12 @@ -111,8 +111,9 @@
    1.13  
    1.14  (* store_theory *)
    1.15  
    1.16 -fun store_theory (thy, name) =
    1.17 +fun store_theory thy =
    1.18    let
    1.19 +    val name = PureThy.get_name thy;
    1.20      val {path, children, parents, thy_time, ml_time, theory = _} =
    1.21        the_thyinfo name;
    1.22      val info = {path = path, children = children, parents = parents,