src/Pure/Thy/thm_deps.ML
changeset 11543 d61b913431c5
parent 11530 b6e21f6cfacd
child 11612 ae8450657bf0
     1.1 --- a/src/Pure/Thy/thm_deps.ML	Fri Aug 31 22:46:23 2001 +0200
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Sat Sep 01 00:14:16 2001 +0200
     1.3 @@ -22,8 +22,8 @@
     1.4  
     1.5  open Proofterm;
     1.6  
     1.7 -fun enable () = keep_derivs := ThmDeriv;
     1.8 -fun disable () = keep_derivs := MinDeriv;
     1.9 +fun enable () = if ! proofs = 0 then proofs := 1 else ();
    1.10 +fun disable () = proofs := 0;
    1.11  
    1.12  fun dest_thm_axm (PThm (nt, prf, _, _)) = (nt, prf)
    1.13    | dest_thm_axm (PAxm (n, _, _)) = ((n ^ " (Ax)", []), MinProof [])