src/Pure/Thy/thy_info.ML
changeset 5209 a69fe5a61b6c
parent 4975 20b89fcd90a7
child 5211 c02b0c727780
     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;