src/HOL/Tools/datatype_package/datatype_rep_proofs.ML
changeset 31643 b040f1679f77
parent 31604 eb2f9d709296
child 31668 a616e56a5ec8
     1.1 --- a/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML	Mon Jun 15 16:13:04 2009 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML	Mon Jun 15 16:13:19 2009 +0200
     1.3 @@ -458,9 +458,9 @@
     1.4        let val isoT = T --> Univ_elT
     1.5        in HOLogic.imp $ 
     1.6          (Const (set_name, UnivT') $ mk_Free "x" Univ_elT i) $
     1.7 -          (if i < length newTs then Const ("True", HOLogic.boolT)
     1.8 +          (if i < length newTs then HOLogic.true_const
     1.9             else HOLogic.mk_mem (mk_Free "x" Univ_elT i,
    1.10 -             Const ("image", [isoT, HOLogic.mk_setT T] ---> UnivT) $
    1.11 +             Const (@{const_name image}, isoT --> HOLogic.mk_setT T --> UnivT) $
    1.12                 Const (iso_name, isoT) $ Const (@{const_name UNIV}, HOLogic.mk_setT T)))
    1.13        end;
    1.14