src/Pure/Thy/thm_deps.ML

--- a/src/Pure/Thy/thm_deps.ML	Fri Aug 31 22:46:23 2001 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Sat Sep 01 00:14:16 2001 +0200
@@ -22,8 +22,8 @@
 
 open Proofterm;
 
-fun enable () = keep_derivs := ThmDeriv;
-fun disable () = keep_derivs := MinDeriv;
+fun enable () = if ! proofs = 0 then proofs := 1 else ();
+fun disable () = proofs := 0;
 
 fun dest_thm_axm (PThm (nt, prf, _, _)) = (nt, prf)
   | dest_thm_axm (PAxm (n, _, _)) = ((n ^ " (Ax)", []), MinProof [])