use_thy_only made pervasive;
authorwenzelm
Tue Apr 27 15:12:34 1999 +0200 (1999-04-27)
changeset 6527f7a7ac2b9926
parent 6526 6b64d1454ee3
child 6528 ed8c5f738ab3
use_thy_only made pervasive;
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/Thy/thy_info.ML	Tue Apr 27 15:10:36 1999 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Tue Apr 27 15:12:34 1999 +0200
     1.3 @@ -26,6 +26,7 @@
     1.4    val use_thy: string -> unit
     1.5    val update_thy: string -> unit
     1.6    val time_use_thy: string -> unit
     1.7 +  val use_thy_only: string -> unit
     1.8  end;
     1.9  
    1.10  signature THY_INFO =
    1.11 @@ -38,7 +39,6 @@
    1.12    val load_file: bool -> Path.T -> unit
    1.13    val use_path: Path.T -> unit
    1.14    val use: string -> unit
    1.15 -  val use_thy_only: string -> unit
    1.16    val begin_theory: string -> string list -> (Path.T * bool) list -> theory
    1.17    val end_theory: theory -> theory
    1.18    val finalize_all: unit -> unit