(tnum,tHOL4.num.num);
(tfun,tHOL4.min.fun);
(tbool,tHOL4.min.bool);
(tlist,tHOL4.list.list);
(tprod,tHOL4.pair.prod);
(treal,tHOL4.realax.real);
(tint,tHOL4.integer.int);
(tind,tHOL4.min.ind);
(threal,tHOL4.hreal.hreal);
(t1,tHOL4.one.one);
   (trecspace,tHOL4.ind_type.recspace);
   (texpression,tHOL4.quote.index);
   (tcform,tHOL4.extreal.extreal);
(toption,tHOL4.option.option);
(tcommand,tHOL4.patricia.ptree);
  (tsetlevel,tHOL4.toto.num_dt);
  (tdirection,tHOL4.frac.frac);
(tcart,tHOL4.fcp.cart);
(tfinite_image,tHOL4.fcp.finite_image);
 (tmultiset,tHOL4.llist.llist);
(tsum,tHOL4.sum.sum);
(ttopology,tHOL4.topology.topology);
  (tquat,tHOL4.ieee.roundmode);
  (ttype,tHOL4.ieee.ccode);
  (tterm,tHOL4.rat.rat);
  (tI,tHOL4.toto.cpn);
  (tind_model,tHOL4.prelim.ordering);
  (tnet,tHOL4.bool.itself)