--- a/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML Mon Jun 15 16:13:04 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML Mon Jun 15 16:13:19 2009 +0200
@@ -458,9 +458,9 @@
let val isoT = T --> Univ_elT
in HOLogic.imp $
(Const (set_name, UnivT') $ mk_Free "x" Univ_elT i) $
- (if i < length newTs then Const ("True", HOLogic.boolT)
+ (if i < length newTs then HOLogic.true_const
else HOLogic.mk_mem (mk_Free "x" Univ_elT i,
- Const ("image", [isoT, HOLogic.mk_setT T] ---> UnivT) $
+ Const (@{const_name image}, isoT --> HOLogic.mk_setT T --> UnivT) $
Const (iso_name, isoT) $ Const (@{const_name UNIV}, HOLogic.mk_setT T)))
end;