thm_count :
     unit ->
     {ASSUME : int, REFL : int, BETA_CONV : int, SUBST : int,
      ABS : int, DISCH : int, MP : int, INST_TYPE : int,
      MK_COMB : int, AP_TERM : int, AP_THM : int, ALPHA : int,
      ETA_CONV : int, SYM : int, TRANS : int, EQ_MP : int,
      EQ_IMP_RULE : int, INST : int, SPEC : int, GEN : int,
      EXISTS : int, CHOOSE : int, CONJ : int, CONJUNCT1 : int,
      CONJUNCT2 : int, DISJ1 : int, DISJ2 : int, DISJ_CASES : int,
      NOT_INTRO : int, NOT_ELIM : int, CCONTR : int, GEN_ABS : int,
      definition : int, axiom : int, from_disk : int, oracle :int,
      total :int }