# HG changeset patch # User kuncar # Date 1338311582 -7200 # Node ID 7599b28b707fcbcc8703b3c507d4071d51f64708 # Parent 6dfe5e77401222d07ed9a301bc64871e29dae7fc don't be so aggressive during unfolding id and o diff -r 6dfe5e774012 -r 7599b28b707f 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).