src/HOL/Tools/datatype_rep_proofs.ML

       in HOLogic.imp $ 
         (Const (set_name, UnivT') $ mk_Free "x" Univ_elT i) $
           (if i < length newTs then Const ("True", HOLogic.boolT)
            else HOLogic.mk_mem (mk_Free "x" Univ_elT i,
              Const ("image", [isoT, HOLogic.mk_setT T] ---> UnivT) $
-               Const (iso_name, isoT) $ Const ("UNIV", HOLogic.mk_setT T)))
+               Const (iso_name, isoT) $ Const (@{const_name UNIV}, HOLogic.mk_setT T)))
       end;
 
     val iso_t = HOLogic.mk_Trueprop (mk_conj (map mk_iso_t
       (rep_set_names ~~ all_rep_names ~~ (0 upto (length descr' - 1)) ~~ recTs)));