use_thy_only made pervasive;
authorwenzelm
Tue, 27 Apr 1999 15:12:34 +0200
changeset 6527 f7a7ac2b9926
parent 6526 6b64d1454ee3
child 6528 ed8c5f738ab3
use_thy_only made pervasive;
src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Apr 27 15:10:36 1999 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Apr 27 15:12:34 1999 +0200
@@ -26,6 +26,7 @@
   val use_thy: string -> unit
   val update_thy: string -> unit
   val time_use_thy: string -> unit
+  val use_thy_only: string -> unit
 end;
 
 signature THY_INFO =
@@ -38,7 +39,6 @@
   val load_file: bool -> Path.T -> unit
   val use_path: Path.T -> unit
   val use: string -> unit
-  val use_thy_only: string -> unit
   val begin_theory: string -> string list -> (Path.T * bool) list -> theory
   val end_theory: theory -> theory
   val finalize_all: unit -> unit