src/Pure/Thy/thy_info.ML
changeset 37871 c7ce7685e087
parent 37216 3165bc303f66
child 37873 66d90b2b87bc
     1.1 --- a/src/Pure/Thy/thy_info.ML	Wed Jul 21 15:23:46 2010 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Jul 21 15:31:38 2010 +0200
     1.3 @@ -16,7 +16,6 @@
     1.4    val if_known_thy: (string -> unit) -> string -> unit
     1.5    val lookup_theory: string -> theory option
     1.6    val get_theory: string -> theory
     1.7 -  val the_theory: string -> theory -> theory
     1.8    val is_finished: string -> bool
     1.9    val master_directory: string -> Path.T
    1.10    val loaded_files: string -> Path.T list
    1.11 @@ -176,10 +175,6 @@
    1.12      SOME theory => theory
    1.13    | _ => error (loader_msg "undefined theory entry for" [name]));
    1.14  
    1.15 -fun the_theory name thy =
    1.16 -  if Context.theory_name thy = name then thy
    1.17 -  else get_theory name;
    1.18 -
    1.19  
    1.20  
    1.21  (** thy operations **)