# 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