src/HOL/Tools/Lifting/lifting_def.ML
changeset 48024 7599b28b707f
parent 47982 7aa35601ff65
child 49625 06cf80661e7a
     1.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Tue May 29 17:06:04 2012 +0200
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Tue May 29 19:13:02 2012 +0200
     1.3 @@ -109,7 +109,7 @@
     1.4  exception CODE_CERT_GEN of string
     1.5  
     1.6  fun simplify_code_eq ctxt def_thm = 
     1.7 -  Local_Defs.unfold ctxt [@{thm o_def}, @{thm map_fun_def}, @{thm id_def}] def_thm
     1.8 +  Local_Defs.unfold ctxt [@{thm o_apply}, @{thm map_fun_def}, @{thm id_apply}] def_thm
     1.9  
    1.10  (*
    1.11    quot_thm - quotient theorem (Quotient R Abs Rep T).