diff -r 6b64d1454ee3 -r f7a7ac2b9926 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