id_const replaces mk_id
authorhaftmann
Tue Dec 21 17:52:23 2010 +0100 (2010-12-21)
changeset 4137348503e4e96b6
parent 41372 551eb49a6e91
child 41374 a35af5180c01
id_const replaces mk_id
src/HOL/Tools/type_lifting.ML
     1.1 --- a/src/HOL/Tools/type_lifting.ML	Tue Dec 21 17:52:23 2010 +0100
     1.2 +++ b/src/HOL/Tools/type_lifting.ML	Tue Dec 21 17:52:23 2010 +0100
     1.3 @@ -124,8 +124,8 @@
     1.4      val Ts' = maps mk_argT (Ts ~~ variances)
     1.5      val T = Type (tyco, Ts);
     1.6      val lhs = list_comb (Const (mapper, Ts' ---> T --> T),
     1.7 -      map (HOLogic.mk_id o domain_type) Ts');
     1.8 -  in (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, HOLogic.mk_id T) end;
     1.9 +      map (HOLogic.id_const o domain_type) Ts');
    1.10 +  in (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, HOLogic.id_const T) end;
    1.11  
    1.12  val comp_apply = Simpdata.mk_eq @{thm o_apply};
    1.13  val id_def = Simpdata.mk_eq @{thm id_def};