src/HOL/Tools/Lifting/lifting_def.ML

--- a/src/HOL/Tools/Lifting/lifting_def.ML	Tue May 29 17:06:04 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Tue May 29 19:13:02 2012 +0200
@@ -109,7 +109,7 @@
 exception CODE_CERT_GEN of string
 
 fun simplify_code_eq ctxt def_thm = 
-  Local_Defs.unfold ctxt [@{thm o_def}, @{thm map_fun_def}, @{thm id_def}] def_thm
+  Local_Defs.unfold ctxt [@{thm o_apply}, @{thm map_fun_def}, @{thm id_apply}] def_thm
 
 (*
   quot_thm - quotient theorem (Quotient R Abs Rep T).