diff -r 228283fa5de4 -r c06825c396e8 src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Thu Oct 07 14:32:32 1999 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Thu Oct 07 14:44:55 1999 +0200
@@ -5,14 +5,25 @@
 Visualize dependencies of theorems.
 *)
 
+signature BASIC_THM_DEPS =
+sig
+  val thm_deps : thm list -> unit
+end;
+
 signature THM_DEPS =
 sig
-  val thm_deps: thm list -> unit
+  include BASIC_THM_DEPS
+
+  val enable : unit -> unit
+  val disable : unit -> unit
 end;
 
 structure ThmDeps : THM_DEPS =
 struct
 
+fun enable () = Thm.keep_derivs := ThmDeriv;
+fun disable () = Thm.keep_derivs := MinDeriv;
+
 fun get_sess thy = if Theory.eq_thy (thy, ProtoPure.thy) then ["Pure"]
   else
     (case #session (Present.get_info thy) of
@@ -69,4 +80,6 @@
 
 end;
 
-open ThmDeps;
+structure BasicThmDeps : BASIC_THM_DEPS = ThmDeps;
+
+open BasicThmDeps;