diff -r 551eb49a6e91 -r 48503e4e96b6 src/HOL/Tools/type_lifting.ML
--- a/src/HOL/Tools/type_lifting.ML	Tue Dec 21 17:52:23 2010 +0100
+++ b/src/HOL/Tools/type_lifting.ML	Tue Dec 21 17:52:23 2010 +0100
@@ -124,8 +124,8 @@
     val Ts' = maps mk_argT (Ts ~~ variances)
     val T = Type (tyco, Ts);
     val lhs = list_comb (Const (mapper, Ts' ---> T --> T),
-      map (HOLogic.mk_id o domain_type) Ts');
-  in (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, HOLogic.mk_id T) end;
+      map (HOLogic.id_const o domain_type) Ts');
+  in (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, HOLogic.id_const T) end;
 
 val comp_apply = Simpdata.mk_eq @{thm o_apply};
 val id_def = Simpdata.mk_eq @{thm id_def};