# HG changeset patch
# User wenzelm
# Date 901638192 -7200
# Node ID a69fe5a61b6cb59654a8e86b8317ec0030b6c98b
# Parent  cea0adbc7276757dcf1fd7840cb429f2fca06498
theory_of renamed to theory (and made public);

diff -r cea0adbc7276 -r a69fe5a61b6c src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Jul 28 17:02:41 1998 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Jul 28 17:03:12 1998 +0200
@@ -28,8 +28,14 @@
            the base of this theory.
 *)
 
+signature BASIC_THY_INFO =
+sig
+  val theory: string -> theory
+end
+
 signature THY_INFO =
 sig
+  include BASIC_THY_INFO
   val loaded_thys: thy_info Symtab.table ref
   val get_thyinfo: string -> thy_info option
   val store_theory: theory -> unit
@@ -37,7 +43,6 @@
   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
   val theory_of_sign: Sign.sg -> theory
   val theory_of_thm: thm -> theory
 end;
@@ -103,7 +108,7 @@
   | None => []);
 
 (*get theory object for a loaded theory*)
-fun theory_of name =
+fun theory name =
   (case get_thyinfo name of
     Some {theory = Some t, ...} => t
   | _ => err_not_stored name);
@@ -124,3 +129,7 @@
 
 
 end;
+
+
+structure BasicThyInfo: BASIC_THY_INFO = ThyInfo;
+open BasicThyInfo;
diff -r cea0adbc7276 -r a69fe5a61b6c src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Tue Jul 28 17:02:41 1998 +0200
+++ b/src/Pure/Thy/thy_read.ML	Tue Jul 28 17:03:12 1998 +0200
@@ -426,7 +426,7 @@
       val base_thy =
        (writeln ("Loading theory " ^ quote child);
          if null mergelist then ProtoPure.thy
-         else Theory.prep_ext_merge (map theory_of mergelist));
+         else Theory.prep_ext_merge (map ThyInfo.theory mergelist));
 
       val dummy =
         let val tinfo = case Symtab.lookup (!loaded_thys, child) of