# HG changeset patch # User kuncar # Date 1393261960 -3600 # Node ID f66371633e1301bf268b2de352bd285608b0dde3 # Parent b6ed5f896ce95f3e1d5df92c239d5ce9c5f3459e be consistent and produce always rep_eq with = diff -r b6ed5f896ce9 -r f66371633e13 src/HOL/Tools/Lifting/lifting_def.ML --- a/src/HOL/Tools/Lifting/lifting_def.ML Mon Feb 24 18:12:40 2014 +0100 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Mon Feb 24 18:12:40 2014 +0100 @@ -265,7 +265,7 @@ val unabs_def = unabs_all_def ctxt unfolded_def in if body_type rty = body_type qty then - SOME (simplify_code_eq ctxt unabs_def) + SOME (simplify_code_eq ctxt (unabs_def RS @{thm meta_eq_to_obj_eq})) else let val thy = Proof_Context.theory_of ctxt