theory_of renamed to theory (and made public);
authorwenzelm
Tue Jul 28 17:03:12 1998 +0200 (1998-07-28)
changeset 5209a69fe5a61b6c
parent 5208 cea0adbc7276
child 5210 54aaa779b6b4
theory_of renamed to theory (and made public);
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_read.ML
     1.1 --- a/src/Pure/Thy/thy_info.ML	Tue Jul 28 17:02:41 1998 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Tue Jul 28 17:03:12 1998 +0200
     1.3 @@ -28,8 +28,14 @@
     1.4             the base of this theory.
     1.5  *)
     1.6  
     1.7 +signature BASIC_THY_INFO =
     1.8 +sig
     1.9 +  val theory: string -> theory
    1.10 +end
    1.11 +
    1.12  signature THY_INFO =
    1.13  sig
    1.14 +  include BASIC_THY_INFO
    1.15    val loaded_thys: thy_info Symtab.table ref
    1.16    val get_thyinfo: string -> thy_info option
    1.17    val store_theory: theory -> unit
    1.18 @@ -37,7 +43,6 @@
    1.19    val children_of: string -> string list
    1.20    val parents_of_name: string -> string list
    1.21    val thyinfo_of_sign: Sign.sg -> string * thy_info
    1.22 -  val theory_of: string -> theory
    1.23    val theory_of_sign: Sign.sg -> theory
    1.24    val theory_of_thm: thm -> theory
    1.25  end;
    1.26 @@ -103,7 +108,7 @@
    1.27    | None => []);
    1.28  
    1.29  (*get theory object for a loaded theory*)
    1.30 -fun theory_of name =
    1.31 +fun theory name =
    1.32    (case get_thyinfo name of
    1.33      Some {theory = Some t, ...} => t
    1.34    | _ => err_not_stored name);
    1.35 @@ -124,3 +129,7 @@
    1.36  
    1.37  
    1.38  end;
    1.39 +
    1.40 +
    1.41 +structure BasicThyInfo: BASIC_THY_INFO = ThyInfo;
    1.42 +open BasicThyInfo;
     2.1 --- a/src/Pure/Thy/thy_read.ML	Tue Jul 28 17:02:41 1998 +0200
     2.2 +++ b/src/Pure/Thy/thy_read.ML	Tue Jul 28 17:03:12 1998 +0200
     2.3 @@ -426,7 +426,7 @@
     2.4        val base_thy =
     2.5         (writeln ("Loading theory " ^ quote child);
     2.6           if null mergelist then ProtoPure.thy
     2.7 -         else Theory.prep_ext_merge (map theory_of mergelist));
     2.8 +         else Theory.prep_ext_merge (map ThyInfo.theory mergelist));
     2.9  
    2.10        val dummy =
    2.11          let val tinfo = case Symtab.lookup (!loaded_thys, child) of