1.1 --- a/src/Pure/Thy/thm_deps.ML	Thu Oct 07 14:32:32 1999 +0200
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Thu Oct 07 14:44:55 1999 +0200
     1.3 @@ -5,14 +5,25 @@
     1.4  Visualize dependencies of theorems.
     1.5  *)
     1.6  
     1.7 +signature BASIC_THM_DEPS =
     1.8 +sig
     1.9 +  val thm_deps : thm list -> unit
    1.10 +end;
    1.11 +
    1.12  signature THM_DEPS =
    1.13  sig
    1.14 -  val thm_deps: thm list -> unit
    1.15 +  include BASIC_THM_DEPS
    1.16 +
    1.17 +  val enable : unit -> unit
    1.18 +  val disable : unit -> unit
    1.19  end;
    1.20  
    1.21  structure ThmDeps : THM_DEPS =
    1.22  struct
    1.23  
    1.24 +fun enable () = Thm.keep_derivs := ThmDeriv;
    1.25 +fun disable () = Thm.keep_derivs := MinDeriv;
    1.26 +
    1.27  fun get_sess thy = if Theory.eq_thy (thy, ProtoPure.thy) then ["Pure"]
    1.28    else
    1.29      (case #session (Present.get_info thy) of
    1.30 @@ -69,4 +80,6 @@
    1.31  
    1.32  end;
    1.33  
    1.34 -open ThmDeps;
    1.35 +structure BasicThmDeps : BASIC_THM_DEPS = ThmDeps;
    1.36 +
    1.37 +open BasicThmDeps;