produce certified vars without access to theory_of_thm, and without context;

produce certified vars without access to theory_of_thm, and without context;

tuned;

added Thm.chyps_of; eliminated Thm.cprep_thm, with its potentially ill-typed (!) tpairs (cf. c9ad3e64ddcf);

prefer theory_id operations; tuned signature;

separate type theory_id;

delete precisely the added rules; tuned;

clarified context;

tuned whitespace;

tuned signature;