src/HOL/Tools/Datatype/datatype.ML
changeset 35402 115a5a95710a
parent 35364 b8c62d60195c
child 35410 1ea89d2a1bd4
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Sat Feb 27 20:56:03 2010 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Sat Feb 27 20:57:08 2010 +0100
     1.3 @@ -465,7 +465,7 @@
     1.4            (if i < length newTs then HOLogic.true_const
     1.5             else HOLogic.mk_mem (mk_Free "x" Univ_elT i,
     1.6               Const (@{const_name image}, isoT --> HOLogic.mk_setT T --> UnivT) $
     1.7 -               Const (iso_name, isoT) $ Const (@{const_name UNIV}, HOLogic.mk_setT T)))
     1.8 +               Const (iso_name, isoT) $ Const (@{const_abbrev UNIV}, HOLogic.mk_setT T)))
     1.9        end;
    1.10  
    1.11      val iso_t = HOLogic.mk_Trueprop (mk_conj (map mk_iso_t